let f, h be UnOps of carr g; :: thesis: ( len f = len (carr g) & ( for i being Element of dom (carr g) holds f . i = comp (g . i) ) & len h = len (carr g) & ( for i being Element of dom (carr g) holds h . i = comp (g . i) ) implies f = h )

assume that

A8: len f = len (carr g) and

A9: for i being Element of dom (carr g) holds f . i = comp (g . i) and

A10: len h = len (carr g) and

A11: for i being Element of dom (carr g) holds h . i = comp (g . i) ; :: thesis: f = h

reconsider f9 = f, h9 = h as FinSequence ;

hence f = h by A8, A10, A12; :: thesis: verum

assume that

A8: len f = len (carr g) and

A9: for i being Element of dom (carr g) holds f . i = comp (g . i) and

A10: len h = len (carr g) and

A11: for i being Element of dom (carr g) holds h . i = comp (g . i) ; :: 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

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

hence f = h by A8, A10, A12; :: thesis: verum