let D be non empty set ; :: thesis: for d being Element of D
for F being FinSequence of D
for g being BinOp of D st len F >= 1 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let d be Element of D; :: thesis: for F being FinSequence of D
for g being BinOp of D st len F >= 1 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let F be FinSequence of D; :: thesis: for g being BinOp of D st len F >= 1 holds
g "**" (F ^ <*d*>) = g . ((g "**" F),d)
let g be BinOp of D; :: thesis: ( len F >= 1 implies g "**" (F ^ <*d*>) = g . ((g "**" F),d) )
set G = F ^ <*d*>;
A1: (F ^ <*d*>) . ((len F) + 1) = d by FINSEQ_1:42;
A2: len (F ^ <*d*>) = (len F) + (len <*d*>) by FINSEQ_1:22
.= (len F) + 1 by FINSEQ_1:39 ;
then 1 <= len (F ^ <*d*>) by NAT_1:12;
then consider f1 being sequence of D such that
A3: f1 . 1 = (F ^ <*d*>) . 1 and
A4: for n being Nat st 0 <> n & n < len (F ^ <*d*>) holds
f1 . (n + 1) = g . ((f1 . n),((F ^ <*d*>) . (n + 1))) and
A5: g "**" (F ^ <*d*>) = f1 . (len (F ^ <*d*>)) by Def1;
assume A6: len F >= 1 ; :: thesis: g "**" (F ^ <*d*>) = g . ((g "**" F),d)
then consider f being sequence of D such that
A7: f . 1 = F . 1 and
A8: for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) and
A9: g "**" F = f . (len F) by Def1;
defpred S₁[ Nat] means ( 0 <> $1 & $1 < len (F ^ <*d*>) implies f . $1 = f1 . $1 );
A10: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A11: S₁[n] ; :: thesis: S₁[n + 1]
assume that
0 <> n + 1 and
A12: n + 1 < len (F ^ <*d*>) ; :: thesis: f . (n + 1) = f1 . (n + 1)
A13: n + 1 >= 1 by NAT_1:14;

now :: thesis: f . (n + 1) = f1 . (n + 1)

per cases ( n + 1 = 1 or n + 1 > 1 ) by A13, XXREAL_0:1;

suppose A14: n + 1 = 1 ; :: thesis: f . (n + 1) = f1 . (n + 1)

1 in dom F by A6, FINSEQ_3:25;
hence f . (n + 1) = f1 . (n + 1) by A7, A3, A14, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A15: n + 1 > 1 ; :: thesis: f . (n + 1) = f1 . (n + 1)

then n <> 0 ;
then A16: f1 . (n + 1) = g . ((f1 . n),((F ^ <*d*>) . (n + 1))) by A4, A12, NAT_1:12;
A17: n + 1 <= len F by A2, A12, NAT_1:13;
then A18: n < len F by NAT_1:13;
1 <= n + 1 by NAT_1:12;
then A19: n + 1 in dom F by A17, FINSEQ_3:25;
n + 1 > 0 + 1 by A15;
then f . (n + 1) = g . ((f . n),(F . (n + 1))) by A8, A18;
hence f . (n + 1) = f1 . (n + 1) by A11, A12, A15, A16, A19, FINSEQ_1:def 7, NAT_1:12; :: thesis: verum

end;

end;

end;

hence f . (n + 1) = f1 . (n + 1) ; :: thesis: verum

end;

A20: S₁[ 0 ] ;
A21: for n being Nat holds S₁[n] from NAT_1:sch 2(A20, A10);
g "**" (F ^ <*d*>) = g . ((f1 . (len F)),((F ^ <*d*>) . ((len F) + 1))) by A6, A2, A4, A5, XREAL_1:29;
hence g "**" (F ^ <*d*>) = g . ((g "**" F),d) by A6, A9, A2, A1, A21, XREAL_1:29; :: thesis: verum