let g be FinSequence of (TOP-REAL 2); :: thesis: for X being Subset of REAL st X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } holds
X = (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))
set T = (TOP-REAL 2) | (L~ g);
set F = proj2 | (L~ g);
let X be Subset of REAL; :: thesis: ( X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } implies X = (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) )
assume A1: X = { (q `2) where q is Point of (TOP-REAL 2) : q in L~ g } ; :: thesis: X = (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))
thus X c= (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) :: according to XBOOLE_0:def 10 :: thesis: (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) )
assume x in X ; :: thesis: x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))
then consider q1 being Point of (TOP-REAL 2) such that
A2: q1 `2 = x and
A3: q1 in L~ g by A1;
A4: x = (proj2 | (L~ g)) . q1 by A2, A3, PSCOMP_1:23;
A5: dom (proj2 | (L~ g)) = the carrier of ((TOP-REAL 2) | (L~ g)) by FUNCT_2:def 1
.= [#] ((TOP-REAL 2) | (L~ g))
.= L~ g by PRE_TOPC:def 5 ;
then q1 in the carrier of ((TOP-REAL 2) | (L~ g)) by A3, FUNCT_2:def 1;
hence x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) by A3, A5, A4, FUNCT_1:def 6; :: thesis: verum
end;
thus (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) or x in X )
assume x in (proj2 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) ; :: thesis: x in X
then consider x1 being object such that
x1 in dom (proj2 | (L~ g)) and
A6: x1 in the carrier of ((TOP-REAL 2) | (L~ g)) and
A7: x = (proj2 | (L~ g)) . x1 by FUNCT_1:def 6;
x1 in [#] ((TOP-REAL 2) | (L~ g)) by A6;
then A8: x1 in L~ g by PRE_TOPC:def 5;
then reconsider x2 = x1 as Element of (TOP-REAL 2) ;
x = x2 `2 by A7, A8, PSCOMP_1:23;
hence x in X by A1, A8; :: thesis: verum
end;