let f, h be MultOps of REAL , carr G; :: thesis: ( len f = len (carr G) & ( for j being Element of dom (carr G) holds f . j = the Mult of (G . j) ) & len h = len (carr G) & ( for j being Element of dom (carr G) holds h . j = the Mult of (G . j) ) implies f = h )

assume that

A21: len f = len (carr G) and

A22: for j being Element of dom (carr G) holds f . j = the Mult of (G . j) and

A23: len h = len (carr G) and

A24: for j being Element of dom (carr G) holds h . j = the Mult of (G . j) ; :: thesis: f = h

reconsider f9 = f, h9 = h as FinSequence ;

hence f = h by A21, A23, A25, FINSEQ_1:13; :: thesis: verum

assume that

A21: len f = len (carr G) and

A22: for j being Element of dom (carr G) holds f . j = the Mult of (G . j) and

A23: len h = len (carr G) and

A24: for j being Element of dom (carr G) holds h . j = the Mult of (G . j) ; :: thesis: f = h

reconsider f9 = f, h9 = h as FinSequence ;

A25: now :: thesis: for i being Nat st i in dom f9 holds

f9 . i = h9 . i

( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) )
by FINSEQ_1:def 3;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 A21, FINSEQ_3:29;

f9 . i = the Mult of (G . i9) by A22;

hence f9 . i = h9 . i by A24; :: thesis: verum

end;assume i in dom f9 ; :: thesis: f9 . i = h9 . i

then reconsider i9 = i as Element of dom (carr G) by A21, FINSEQ_3:29;

f9 . i = the Mult of (G . i9) by A22;

hence f9 . i = h9 . i by A24; :: thesis: verum

hence f = h by A21, A23, A25, FINSEQ_1:13; :: thesis: verum