let f, h be BinOps of carr g; :: thesis: ( len f = len (carr g) & ( for i being Element of dom (carr g) holds f . i = the addF of (g . i) ) & len h = len (carr g) & ( for i being Element of dom (carr g) holds h . i = the addF of (g . i) ) implies f = h )
assume that
A2: ( len f = len (carr g) & ( for i being Element of dom (carr g) holds f . i = the addF of (g . i) ) ) and
A3: ( len h = len (carr g) & ( for i being Element of dom (carr g) holds h . i = the addF of (g . i) ) ) ; :: thesis: f = h
reconsider f' = f, h' = h as FinSequence ;
A4: ( dom f' = Seg (len f') & dom h' = Seg (len h') ) by FINSEQ_1:def 3;

now

let i be Nat; :: thesis: ( i in dom f' implies f' . i = h' . i )
assume i in dom f' ; :: thesis: f' . i = h' . i
then reconsider i' = i as Element of dom (carr g) by A2, FINSEQ_3:31;
f' . i = the addF of (g . i') by A2;
hence f' . i = h' . i by A3; :: thesis: verum

end;

hence f = h by A2, A3, A4, FINSEQ_1:17; :: thesis: verum