let K1 be non empty Subset of (TOP-REAL 2); :: thesis: for q being Point of ((TOP-REAL 2) | K1) holds (proj2 | K1) . q = proj2 . q

let q be Point of ((TOP-REAL 2) | K1); :: thesis: (proj2 | K1) . q = proj2 . 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 proj2) /\ K1 by Lm3, XBOOLE_0:def 4;

hence (proj2 | K1) . q = proj2 . q by FUNCT_1:48; :: thesis: verum

let q be Point of ((TOP-REAL 2) | K1); :: thesis: (proj2 | K1) . q = proj2 . 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 proj2) /\ K1 by Lm3, XBOOLE_0:def 4;

hence (proj2 | K1) . q = proj2 . q by FUNCT_1:48; :: thesis: verum