let K1 be non empty Subset of (TOP-REAL 2); :: thesis: for q being Point of ((TOP-REAL 2) | K1) holds (proj1 | K1) . q = proj1 . q
let q be Point of ((TOP-REAL 2) | K1); :: thesis: (proj1 | K1) . q = proj1 . q
( the carrier of ((TOP-REAL 2) | K1) = K1 & q in the carrier of ((TOP-REAL 2) | K1) ) by PRE_TOPC:8;
then q in (dom proj1) /\ K1 by Lm2, XBOOLE_0:def 4;
hence (proj1 | K1) . q = proj1 . q by FUNCT_1:48; :: thesis: verum