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 = (Re (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 = (Re (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 = (Re (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 = (Re (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 = (Re (f # x)) . n ) ) ; :: thesis: g = h

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

let n be Element of NAT ; :: thesis: g . n = h . n
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

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 = (Re (f # x)) . n by A6;
hence (g . n) . x = (h . n) . x by A7, A8, A9; :: thesis: verum

end;

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

end;

hence g = h by FUNCT_2:63; :: thesis: verum