let n be non zero Nat; :: thesis: n = (TSqF n) * (n div (TSqF n))
TSqF n divides n by MOEBIUS2:53;
then A2: n mod (TSqF n) = 0 by INT_1:62;
set i2 = TSqF n;
n = ((n div (TSqF n)) * (TSqF n)) + (n mod (TSqF n)) by INT_1:59
.= (n div (TSqF n)) * (TSqF n) by A2 ;
hence n = (TSqF n) * (n div (TSqF n)) ; :: thesis: verum