consider k being Nat such that
Z2: n = (TSqF n) * k by NAT_D:def 3, Skup;
n div (TSqF n) = k by NAT_D:18, Z2;
then Z1: n div (TSqF n) <> 0 by Z2;
for p being Prime holds p |-count (n div (TSqF n)) <= 1
proof
let p be Prime; :: thesis: p |-count (n div (TSqF n)) <= 1
XX: p <> 1 by INT_2:def 4;
reconsider b = TSqF n as non zero Nat ;
S1: p |-count (n div b) = (p |-count n) -' (p |-count b) by Skup, NAT_3:31;
set h = 2 * ((p |-count n) div 2);
per cases ( p in support (pfexp n) or not p in support (pfexp n) ) ;
end;
end;
hence for b1 being Nat st b1 = n div (TSqF n) holds
not b1 is square-containing by Z1, MoInv; :: thesis: verum