let f, h be UnOps of carr G; :: thesis: ( len f = len (carr G) & ( for j being Element of dom (carr G) holds f . j = comp (G . j) ) & len h = len (carr G) & ( for j being Element of dom (carr G) holds h . j = comp (G . j) ) implies f = h )
assume that
A8: len f = len (carr G) and
A9: for j being Element of dom (carr G) holds f . j = comp (G . j) and
A10: len h = len (carr G) and
A11: for j being Element of dom (carr G) holds h . j = comp (G . j) ; :: thesis: f = h
reconsider f9 = f, h9 = h as FinSequence ;

A12: now :: thesis: for i being Nat st i in dom f9 holds
f . i = h . i

let i be Nat; :: thesis: ( i in dom f9 implies f . i = h . i )
assume i in dom f9 ; :: thesis: f . i = h . i
then reconsider i9 = i as Element of dom (carr G) by A8, FINSEQ_3:29;
f . i = comp (G . i9) by A9;
hence f . i = h . i by A11; :: thesis: verum

end;

( dom f9 = Seg (len f9) & dom h9 = Seg (len h9) ) by FINSEQ_1:def 3;
hence f = h by A8, A10, A12, FINSEQ_1:13; :: thesis: verum