let D be non empty set ; :: thesis: for F being XFinSequence of D
for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds
b "**" F = b "**" (XFS2FS F)
let F be XFinSequence of D; :: thesis: for b being BinOp of D st ( b is having_a_unity or len F >= 1 ) holds
b "**" F = b "**" (XFS2FS F)
let b be BinOp of D; :: thesis: ( ( b is having_a_unity or len F >= 1 ) implies b "**" F = b "**" (XFS2FS F) )
assume A1: ( b is having_a_unity or len F >= 1 ) ; :: thesis: b "**" F = b "**" (XFS2FS F)

per cases ( len F >= 1 or ( b is having_a_unity & len F < 1 ) ) by A1;

suppose A2: len F >= 1 ; :: thesis: b "**" F = b "**" (XFS2FS F)

set FS = XFS2FS F;
len F = len (XFS2FS F) by AFINSQ_1:def 9;
then consider f being Function of NAT,D such that
A3: f . 1 = (XFS2FS F) . 1 and
A4: for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = b . ((f . n),((XFS2FS F) . (n + 1))) and
A5: b "**" (XFS2FS F) = f . (len F) by A2, FINSOP_1:def 1;
consider xf being Function of NAT,D such that
A6: xf . 0 = F . 0 and
A7: for n being Nat st n + 1 < len F holds
xf . (n + 1) = b . ((xf . n),(F . (n + 1))) and
A8: b "**" F = xf . ((len F) - 1) by A2, Def9;
defpred S₁[ Nat] means ( $1 < len F implies xf . $1 = f . ($1 + 1) );
A9: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A10: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
set n2 = (n + 1) + 1;
assume A11: n + 1 < len F ; :: thesis: xf . (n + 1) = f . ((n + 1) + 1)
then ( 0 + 1 <= (n + 1) + 1 & (n + 1) + 1 <= len F ) by NAT_1:13;
then A12: F . (((n + 1) + 1) -' 1) = (XFS2FS F) . ((n + 1) + 1) by AFINSQ_1:def 9;
( xf . (n + 1) = b . ((xf . n),(F . (n + 1))) & f . ((n + 1) + 1) = b . ((f . (n + 1)),((XFS2FS F) . ((n + 1) + 1))) ) by A7, A4, A11;
hence xf . (n + 1) = f . ((n + 1) + 1) by A10, A11, A12, NAT_1:13, NAT_D:34; :: thesis: verum

end;

reconsider L1 = (len F) - 1 as Element of NAT by A2, NAT_1:21;
A13: L1 < L1 + 1 by NAT_1:13;
A14: S₁[ 0 ]

proof

assume 0 < len F ; :: thesis: xf . 0 = f . (0 + 1)
then 0 + 1 <= len F by NAT_1:13;
then F . (1 -' 1) = (XFS2FS F) . 1 by AFINSQ_1:def 9;
hence xf . 0 = f . (0 + 1) by A6, A3, XREAL_1:232; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A14, A9);
hence b "**" F = b "**" (XFS2FS F) by A8, A5, A13; :: thesis: verum

end;

suppose A15: ( b is having_a_unity & len F < 1 ) ; :: thesis: b "**" F = b "**" (XFS2FS F)

then len F <= 0 + 1 ;
then A16: len F = 0 by A15, NAT_1:8;
then ( len F = len (XFS2FS F) & b "**" F = the_unity_wrt b ) by A15, Def9, AFINSQ_1:def 9;
hence b "**" F = b "**" (XFS2FS F) by A15, A16, FINSOP_1:def 1; :: thesis: verum

end;

end;