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
A1: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
q in the carrier of ((TOP-REAL 2) | K1) ;
then q in (dom proj1 ) /\ K1 by A1, Lm2, XBOOLE_0:def 4;
hence (proj1 | K1) . q = proj1 . q by FUNCT_1:71; :: thesis: verum