let f be complex-valued XFinSequence; :: thesis: Product (XFS2FS f) = XProduct f
reconsider n = len f as Nat ;
defpred S₁[ Nat] means Product (XFS2FS (f | $1)) = XProduct (f | $1);
A1: S₁[ 0 ]

proof

1 * (Product (XFS2FS (f | 0))) = XProduct (f | 0) by PFO;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: S₁[k] ; :: thesis: S₁[k + 1]
reconsider g = <%(f . k)%> as complex-valued XFinSequence ;

per cases ( k in dom f or not k in dom f ) ;

suppose C0: k in dom f ; :: thesis: S₁[k + 1]

then C1: k + 1 <= len f by NAT_1:13, AFINSQ_1:86;
( (f | (k + 1)) | k = f | k & (f | (k + 1)) . k = f . k ) by CNM, CNX;
then f | (k + 1) = (f | k) ^ <%(f . k)%> by C1, AFINSQ_1:54, AFINSQ_1:56;
then Product (XFS2FS (f | (k + 1))) = Product ((XFS2FS (f | k)) ^ (XFS2FS <%(f . k)%>)) by SXX
.= (Product (XFS2FS (f | k))) * (Product (XFS2FS <%(f . k)%>)) by FAF
.= (XProduct (f | k)) * (Product <*(f . k)*>) by B1, XCF
.= XProduct (f | (k + 1)) by C0, A265 ;
hence S₁[k + 1] ; :: thesis: verum

end;

suppose not k in dom f ; :: thesis: S₁[k + 1]

then C1: k >= len f by AFINSQ_1:86;
k + 1 >= k + 0 by XREAL_1:6;
then ( f | k = f & f | (k + 1) = f ) by C1, XXREAL_0:2, AFINSQ_1:52;
hence S₁[k + 1] by B1; :: thesis: verum

end;

end;

end;

for x being Nat holds S₁[x] from NAT_1:sch 2(A1, A2);
then Product (XFS2FS (f | n)) = XProduct (f | n) ;
hence Product (XFS2FS f) = XProduct f ; :: thesis: verum