let g be FinSequence of (); :: thesis: for X being Subset of REAL st X = { (q `1) where q is Point of () : q in L~ g } holds
X = (proj1 | (L~ g)) .: the carrier of (() | (L~ g))

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