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) and
A3: for i being Element of dom (carr g) holds f . i = the addF of (g . i) and
A4: len h = len (carr g) and
A5: for i being Element of dom (carr g) holds h . i = the addF of (g . i) ; :: thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;

A6: now :: thesis: for i being Nat st i in dom f9 holds
f9 . i = h9 . i

let i be Nat; :: thesis: ( i in dom f9 implies f9 . i = h9 . i )
assume i in dom f9 ; :: thesis: f9 . i = h9 . i
then reconsider i9 = i as Element of dom (carr g) by A2, FINSEQ_3:29;
f9 . i = the addF of (g . i9) by A3;
hence f9 . i = h9 . i by A5; :: thesis: verum

end;

( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def 3;
hence f = h by A2, A4, A6; :: thesis: verum