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)

then consider xf being Function of NAT ,D such that
A3: xf . 0 = F . 0 and
A4: for n being Element of NAT st n + 1 < len F holds
xf . (n + 1) = b . (xf . n),(F . (n + 1)) and
A5: b "**" F = xf . ((len F) - 1) by STIRL2_1:def 3;
set FS = XFS2FS F;
( len (XFS2FS F) >= 1 & len F = len (XFS2FS F) ) by A2, PRGCOR_2:def 2;
then consider f being Function of NAT ,D such that
A6: f . 1 = (XFS2FS F) . 1 and
A7: for n being Element of NAT st 0 <> n & n < len F holds
f . (n + 1) = b . (f . n),((XFS2FS F) . (n + 1)) and
A8: b "**" (XFS2FS F) = f . (len F) by FINSOP_1:def 1;
defpred S₁[ Element of NAT ] means ( $1 < len F implies xf . $1 = f . ($1 + 1) );
A9: 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 & 1 -' 1 = 0 ) by PRGCOR_2:def 2, XREAL_1:234;
hence xf . 0 = f . (0 + 1) by A3, A6; :: thesis: verum

end;

A10: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

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

end;

A13: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A9, A10);
reconsider L1 = (len F) - 1 as Element of NAT by A2, NAT_1:21;
L1 < L1 + 1 by NAT_1:13;
hence b "**" F = b "**" (XFS2FS F) by A5, A8, A13; :: thesis: verum

end;

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

then len F <= 0 + 1 ;
then ( len F = 1 or len F <= 0 ) by NAT_1:8;
then ( len F = 0 & len F = len (XFS2FS F) ) by A14, PRGCOR_2:def 2;
then ( b "**" F = the_unity_wrt b & b "**" (XFS2FS F) = the_unity_wrt b ) by A14, FINSOP_1:def 1, STIRL2_1:def 3;
hence b "**" F = b "**" (XFS2FS F) ; :: thesis: verum

end;

end;