for n being Nat holds (rseq (0,1,1,0)) . n = (Reci-Sqf . n) * (Reci-TSq . n)

proof

let n be Nat; :: thesis: (rseq (0,1,1,0)) . n = (Reci-Sqf . n) * (Reci-TSq . n)
A1: (rseq (0,1,1,0)) . n = 1 / ((1 * n) + 0) by AlgDef;

per cases ( n = 0 or n <> 0 ) ;

suppose A2: n = 0 ; :: thesis: (rseq (0,1,1,0)) . n = (Reci-Sqf . n) * (Reci-TSq . n)

then (rseq (0,1,1,0)) . n = 1 / ((1 * 0) + 0) by AlgDef
.= (Reci-Sqf . n) * 0
.= (Reci-Sqf . n) * (Reci-TSq . n) by MySum2Def, A2 ;
hence (rseq (0,1,1,0)) . n = (Reci-Sqf . n) * (Reci-TSq . n) ; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: (rseq (0,1,1,0)) . n = (Reci-Sqf . n) * (Reci-TSq . n)

then reconsider nn = n as non zero Nat ;
A3: TSqF nn = (SqF nn) |^ 2 by Cosik
.= (SqF nn) ^2 by NEWTON:81 ;
A4: Reci-TSq . nn = 1 / (TSqF nn) by MySum2Def;
1 / nn = 1 / ((SquarefreePart nn) * (TSqF nn)) by Canonical, A3
.= (1 / (SquarefreePart nn)) * (1 / (TSqF nn)) by XCMPLX_1:102 ;
hence (rseq (0,1,1,0)) . n = (Reci-Sqf . n) * (Reci-TSq . n) by MySumDef, A1, A4; :: thesis: verum

end;

end;

end;

hence rseq (0,1,1,0) = Reci-Sqf (#) Reci-TSq by SEQ_1:8; :: thesis: verum