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 f' = f, h' = h as FinSequence ;

A25: 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 A21, FINSEQ_3:31;
f' . i = the Mult of (G . i') by A22;
hence f' . i = h' . i by A24; :: thesis: verum

end;

( dom f' = Seg (len f') & dom h' = Seg (len h') ) by FINSEQ_1:def 3;
hence f = h by A21, A23, A25, FINSEQ_1:17; :: thesis: verum