let D be non empty set ; :: thesis: for F being BinOp of D
for i being Nat st F is having_a_unity holds
F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F
let F be BinOp of D; :: thesis: for i being Nat st F is having_a_unity holds
F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F
let i be Nat; :: thesis: ( F is having_a_unity implies F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F )
assume A1: F is having_a_unity ; :: thesis: F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F
set e = the_unity_wrt F;
defpred S₁[ Nat] means F "**" ($1 |-> (the_unity_wrt F)) = the_unity_wrt F;
F "**" (0 |-> (the_unity_wrt F)) = F "**" (<*> D) by FINSEQ_2:72
.= the_unity_wrt F by A1, FINSOP_1:11 ;
then A2: S₁[ 0 ] ;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F ; :: thesis: S₁[i + 1]
thus F "**" ((i + 1) |-> (the_unity_wrt F)) = F "**" ((i |-> (the_unity_wrt F)) ^ <*(the_unity_wrt F)*>) by FINSEQ_2:74
.= F . (F "**" (i |-> (the_unity_wrt F))),(the_unity_wrt F) by A1, FINSOP_1:5
.= the_unity_wrt F by A1, A4, SETWISEO:23 ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F ; :: thesis: verum