let g be FinSequence of (TOP-REAL 2); :: thesis: for X being Subset of REAL st X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } holds

X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))

set T = (TOP-REAL 2) | (L~ g);

set F = proj1 | (L~ g);

let X be Subset of REAL; :: thesis: ( X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } implies X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) )

assume A1: X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } ; :: thesis: X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))

thus X c= (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) :: according to XBOOLE_0:def 10 :: thesis: (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X

X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))

set T = (TOP-REAL 2) | (L~ g);

set F = proj1 | (L~ g);

let X be Subset of REAL; :: thesis: ( X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } implies X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) )

assume A1: X = { (q `1) where q is Point of (TOP-REAL 2) : q in L~ g } ; :: thesis: X = (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))

thus X c= (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) :: according to XBOOLE_0:def 10 :: thesis: (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X

proof

thus
(proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) c= X
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) )

assume x in X ; :: thesis: x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))

then consider q1 being Point of (TOP-REAL 2) such that

A2: q1 `1 = x and

A3: q1 in L~ g by A1;

A4: x = (proj1 | (L~ g)) . q1 by A2, A3, PSCOMP_1:22;

A5: dom (proj1 | (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 (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) by A3, A5, A4, FUNCT_1:def 6; :: thesis: verum

end;assume x in X ; :: thesis: x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g))

then consider q1 being Point of (TOP-REAL 2) such that

A2: q1 `1 = x and

A3: q1 in L~ g by A1;

A4: x = (proj1 | (L~ g)) . q1 by A2, A3, PSCOMP_1:22;

A5: dom (proj1 | (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 (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) by A3, A5, A4, FUNCT_1:def 6; :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) or x in X )

assume x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) ; :: thesis: x in X

then consider x1 being object such that

x1 in dom (proj1 | (L~ g)) and

A6: x1 in the carrier of ((TOP-REAL 2) | (L~ g)) and

A7: x = (proj1 | (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 `1 by A7, A8, PSCOMP_1:22;

hence x in X by A1, A8; :: thesis: verum

end;assume x in (proj1 | (L~ g)) .: the carrier of ((TOP-REAL 2) | (L~ g)) ; :: thesis: x in X

then consider x1 being object such that

x1 in dom (proj1 | (L~ g)) and

A6: x1 in the carrier of ((TOP-REAL 2) | (L~ g)) and

A7: x = (proj1 | (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 `1 by A7, A8, PSCOMP_1:22;

hence x in X by A1, A8; :: thesis: verum