let H1, H2 be FinSequence-yielding Function; :: thesis: ( dom H1 = doms F & ( for p being FinSequence st p in doms F holds
( len (H1 . p) = len p & ( for i being Nat st i in dom p holds
(H1 . p) . i = (F . i) . (p . i) ) ) ) & dom H2 = doms F & ( for p being FinSequence st p in doms F holds
( len (H2 . p) = len p & ( for i being Nat st i in dom p holds
(H2 . p) . i = (F . i) . (p . i) ) ) ) implies H1 = H2 )
assume that
A7: ( dom H1 = doms F & ( for p being FinSequence st p in doms F holds
( len (H1 . p) = len p & ( for i being Nat st i in dom p holds
(H1 . p) . i = (F . i) . (p . i) ) ) ) ) and
A8: ( dom H2 = doms F & ( for p being FinSequence st p in doms F holds
( len (H2 . p) = len p & ( for i being Nat st i in dom p holds
(H2 . p) . i = (F . i) . (p . i) ) ) ) ) ; :: thesis: H1 = H2
for x being object st x in dom H1 holds
H1 . x = H2 . x

proof

let x be object ; :: thesis: ( x in dom H1 implies H1 . x = H2 . x )
assume A9: x in dom H1 ; :: thesis: H1 . x = H2 . x
reconsider p = x as FinSequence by A9, A7;
A10: ( len (H1 . p) = len p & len p = len (H2 . p) ) by A7, A8, A9;
then A11: ( dom (H1 . p) = dom p & dom p = dom (H2 . p) ) by FINSEQ_3:29;

now :: thesis: for i being Nat st i in dom (H1 . p) holds
(H1 . p) . i = (H2 . p) . i

let i be Nat; :: thesis: ( i in dom (H1 . p) implies (H1 . p) . i = (H2 . p) . i )
assume A12: i in dom (H1 . p) ; :: thesis: (H1 . p) . i = (H2 . p) . i
then (H1 . p) . i = (F . i) . (p . i) by A11, A9, A7;
hence (H1 . p) . i = (H2 . p) . i by A11, A12, A9, A7, A8; :: thesis: verum

end;

hence H1 . x = H2 . x by A10, FINSEQ_3:29; :: thesis: verum

end;

hence H1 = H2 by A7, A8; :: thesis: verum