let g, h be Functional_Sequence of X,REAL; :: thesis: ( ( for n being Nat holds

( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds

(g . n) . x = (Im (f # x)) . n ) ) ) & ( for n being Nat holds

( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds

(h . n) . x = (Im (f # x)) . n ) ) ) implies g = h )

assume A6: for n being Nat holds

( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds

(g . n) . x = (Im (f # x)) . n ) ) ; :: thesis: ( ex n being Nat st

( dom (h . n) = dom (f . n) implies ex x being Element of X st

( x in dom (h . n) & not (h . n) . x = (Im (f # x)) . n ) ) or g = h )

assume A7: for n being Nat holds

( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds

(h . n) . x = (Im (f # x)) . n ) ) ; :: thesis: g = h

( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds

(g . n) . x = (Im (f # x)) . n ) ) ) & ( for n being Nat holds

( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds

(h . n) . x = (Im (f # x)) . n ) ) ) implies g = h )

assume A6: for n being Nat holds

( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds

(g . n) . x = (Im (f # x)) . n ) ) ; :: thesis: ( ex n being Nat st

( dom (h . n) = dom (f . n) implies ex x being Element of X st

( x in dom (h . n) & not (h . n) . x = (Im (f # x)) . n ) ) or g = h )

assume A7: for n being Nat holds

( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds

(h . n) . x = (Im (f # x)) . n ) ) ; :: thesis: g = h

now :: thesis: for n being Element of NAT holds g . n = h . n

hence
g = h
by FUNCT_2:63; :: thesis: verumlet n be Element of NAT ; :: thesis: g . n = h . n

A8: dom (g . n) = dom (f . n) by A6

.= dom (h . n) by A7 ;

end;A8: dom (g . n) = dom (f . n) by A6

.= dom (h . n) by A7 ;

now :: thesis: for x being Element of X st x in dom (g . n) holds

(g . n) . x = (h . n) . x

hence
g . n = h . n
by A8, PARTFUN1:5; :: thesis: verum(g . n) . x = (h . n) . x

let x be Element of X; :: thesis: ( x in dom (g . n) implies (g . n) . x = (h . n) . x )

assume A9: x in dom (g . n) ; :: thesis: (g . n) . x = (h . n) . x

then (g . n) . x = (Im (f # x)) . n by A6;

hence (g . n) . x = (h . n) . x by A7, A8, A9; :: thesis: verum

end;assume A9: x in dom (g . n) ; :: thesis: (g . n) . x = (h . n) . x

then (g . n) . x = (Im (f # x)) . n by A6;

hence (g . n) . x = (h . n) . x by A7, A8, A9; :: thesis: verum