let Z1, Z2 be Subset of ExtREAL ; :: thesis: ( ( for z being R_eal holds
( z in Z1 iff ex x, y being R_eal st
( x in X & y in Y & z = x + y ) ) ) & ( for z being R_eal holds
( z in Z2 iff ex x, y being R_eal st
( x in X & y in Y & z = x + y ) ) ) implies Z1 = Z2 )
assume that
A2: for z being R_eal holds
( z in Z1 iff ex x, y being R_eal st
( x in X & y in Y & z = x + y ) ) and
A3: for z being R_eal holds
( z in Z2 iff ex x, y being R_eal st
( x in X & y in Y & z = x + y ) ) ; :: thesis: Z1 = Z2
for z being set holds
( z in Z1 iff z in Z2 )

proof

let z be set ; :: thesis: ( z in Z1 iff z in Z2 )

hereby :: thesis: ( z in Z2 implies z in Z1 )

assume A4: z in Z1 ; :: thesis: z in Z2
then reconsider z' = z as R_eal ;
ex x, y being R_eal st
( x in X & y in Y & z' = x + y ) by A2, A4;
hence z in Z2 by A3; :: thesis: verum

end;

assume A5: z in Z2 ; :: thesis: z in Z1
then reconsider z = z as R_eal ;
ex x, y being R_eal st
( x in X & y in Y & z = x + y ) by A3, A5;
hence z in Z1 by A2; :: thesis: verum

end;

hence Z1 = Z2 by TARSKI:2; :: thesis: verum