let K1 be non empty Subset of (TOP-REAL 2); :: thesis: for g1 being Function of ((TOP-REAL 2) | K1),R^1 st g1 = (2 NormF) | K1 & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q <> 0. (TOP-REAL 2) ) holds
for q being Point of ((TOP-REAL 2) | K1) holds g1 . q <> 0
let g1 be Function of ((TOP-REAL 2) | K1),R^1; :: thesis: ( g1 = (2 NormF) | K1 & ( for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q <> 0. (TOP-REAL 2) ) implies for q being Point of ((TOP-REAL 2) | K1) holds g1 . q <> 0 )
assume that
A1: g1 = (2 NormF) | K1 and
A2: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K1) holds
q <> 0. (TOP-REAL 2) ; :: thesis: for q being Point of ((TOP-REAL 2) | K1) holds g1 . q <> 0
let q be Point of ((TOP-REAL 2) | K1); :: thesis: g1 . q <> 0
( the carrier of ((TOP-REAL 2) | K1) = K1 & q in the carrier of ((TOP-REAL 2) | K1) ) by PRE_TOPC:8;
then reconsider q2 = q as Point of (TOP-REAL 2) ;
g1 . q = (2 NormF) . q by A1, Lm5
.= |.q2.| by Def1 ;
hence g1 . q <> 0 by A2, TOPRNS_1:24; :: thesis: verum