let g, h be with_the_same_dom Functional_Sequence of X,ExtREAL ; :: thesis: ( ( for n being natural number 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 natural number 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 A8: for n being natural number 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 natural number 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 A9: for n being natural number 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

let n be Element of NAT ; :: thesis: g . n = h . n
A10: dom (g . n) = dom (f . 0 ) by A8
.= dom (h . n) by A9 ;

now

let x be Element of X; :: thesis: ( x in dom (g . n) implies (g . n) /. x = (h . n) /. x )
assume A11: x in dom (g . n) ; :: thesis: (g . n) /. x = (h . n) /. x
then (g . n) /. x = (g . n) . x by PARTFUN1:def 8;
then (g . n) /. x = (inferior_realsequence (f # x)) . n by A8, A11;
then (g . n) /. x = (h . n) . x by A9, A10, A11;
hence (g . n) /. x = (h . n) /. x by A10, A11, PARTFUN1:def 8; :: thesis: verum

end;

hence g . n = h . n by A10, PARTFUN2:3; :: thesis: verum

end;

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