let p1, p2 be Real_Sequence; :: thesis: ( ( for i being Nat holds p1 . i = (g . i) . x ) & ( for i being Nat holds p2 . i = (g . i) . x ) implies p1 = p2 )
assume B1: ( ( for i being Nat holds p1 . i = (g . i) . x ) & ( for i being Nat holds p2 . i = (g . i) . x ) ) ; :: thesis: p1 = p2
B2: ( dom p1 = NAT & dom p2 = NAT ) by FUNCT_2:def 1;

now :: thesis: for i being object st i in dom p1 holds
p1 . i = p2 . i

let i be object ; :: thesis: ( i in dom p1 implies p1 . i = p2 . i )
assume i in dom p1 ; :: thesis: p1 . i = p2 . i
then reconsider i1 = i as Nat ;
p1 . i = (g . i1) . x by B1;
hence p1 . i = p2 . i by B1; :: thesis: verum

end;

hence p1 = p2 by B2; :: thesis: verum