let g, h be with_the_same_dom Functional_Sequence of X,ExtREAL; :: thesis: ( ( for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) ) ) & ( for n being Nat holds
( dom (h . n) = dom (f . 0) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (inferior_realsequence (f # x)) . n ) ) ) implies g = h )
assume A7: for n being Nat holds
( dom (g . n) = dom (f . 0) & ( for x being Element of X st x in dom (g . n) holds
(g . n) . x = (inferior_realsequence (f # x)) . n ) ) ; :: thesis: ( ex n being Nat st
( dom (h . n) = dom (f . 0) implies ex x being Element of X st
( x in dom (h . n) & not (h . n) . x = (inferior_realsequence (f # x)) . n ) ) or g = h )
assume A8: for n being Nat holds
( dom (h . n) = dom (f . 0) & ( for x being Element of X st x in dom (h . n) holds
(h . n) . x = (inferior_realsequence (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
A9: dom (g . n) = dom (f . 0) by A7
.= dom (h . n) by A8 ;

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 A10: x in dom (g . n) ; :: thesis: (g . n) /. x = (h . n) /. x
then (g . n) /. x = (g . n) . x by PARTFUN1:def 6;
then (g . n) /. x = (inferior_realsequence (f # x)) . n by A7, A10;
then (g . n) /. x = (h . n) . x by A8, A9, A10;
hence (g . n) /. x = (h . n) /. x by A9, A10, PARTFUN1:def 6; :: thesis: verum

end;

hence g . n = h . n by A9, PARTFUN2:1; :: thesis: verum

end;

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