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) ) ;

suppose K1: p in support (pfexp n) ; :: thesis: p |-count (n div (TSqF n)) <= 1

then s: (TSqFactors n) . p = p |^ (2 * ((p |-count n) div 2)) by TSqDef;
p divides n by K1, NAT_3:36;
then p |-count n <> 0 by NAT_3:27, XX;
then S4: (p |-count n) - (2 * ((p |-count n) div 2)) <= 1 by FOT1;
(p |-count n) - (p |-count b) <= (p |-count n) - (2 * ((p |-count n) div 2)) by s, BZE, XREAL_1:10;
then (p |-count n) - (p |-count b) <= 1 by S4, XXREAL_0:2;
hence p |-count (n div (TSqF n)) <= 1 by S1, XREAL_0:def 2; :: thesis: verum

end;

suppose not p in support (pfexp n) ; :: thesis: p |-count (n div (TSqF n)) <= 1

then not p divides n by NAT_3:37;
then p |-count n = 0 by XX, NAT_3:27;
hence p |-count (n div (TSqF n)) <= 1 by S1; :: thesis: verum

end;

end;

end;

hence for b₁ being Nat st b₁ = n div (TSqF n) holds
not b₁ is square-containing by Z1, MoInv; :: thesis: verum