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 )
set e = the_unity_wrt F;
defpred S₁[ Nat] means F "**" ($1 |-> (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
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: 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:60
.= F . ((F "**" (i |-> (the_unity_wrt F))),(the_unity_wrt F)) by A1, FINSOP_1:4
.= the_unity_wrt F by A1, A3, SETWISEO:15 ; :: thesis: verum

end;

F "**" (0 |-> (the_unity_wrt F)) = F "**" (<*> D)
.= the_unity_wrt F by A1, FINSOP_1:10 ;
then A4: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A4, A2);
hence F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F ; :: thesis: verum