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_{1}[ 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_{1}[i] holds

S_{1}[i + 1]

.= the_unity_wrt F by A1, FINSOP_1:10 ;

then A4: S_{1}[ 0 ]
;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A4, A2);

hence F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F ; :: thesis: verum

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

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

S

proof

F "**" (0 |-> (the_unity_wrt F)) =
F "**" (<*> D)
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A3: F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F ; :: thesis: S_{1}[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;assume A3: F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F ; :: thesis: S

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

.= the_unity_wrt F by A1, FINSOP_1:10 ;

then A4: S

for i being Nat holds S

hence F "**" (i |-> (the_unity_wrt F)) = the_unity_wrt F ; :: thesis: verum