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 )
A1: the carrier of ((TOP-REAL 2) | K1) = K1 by PRE_TOPC:29;
assume A2: ( 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) ) ) ; :: 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
q in the carrier of ((TOP-REAL 2) | K1) ;
then reconsider q2 = q as Point of (TOP-REAL 2) by A1;
g1 . q = (2 NormF ) . q by A2, Lm5
.= |.q2.| by Def1 ;
hence g1 . q <> 0 by A2, TOPRNS_1:25; :: thesis: verum