let S, T be non empty TopSpace; :: thesis: for Z being non empty SubSpace of T
for f being Function of S,T
for g being Function of S,Z st f = g & f is open holds
g is open
let Z be non empty SubSpace of T; :: thesis: for f being Function of S,T
for g being Function of S,Z st f = g & f is open holds
g is open
let f be Function of S,T; :: thesis: for g being Function of S,Z st f = g & f is open holds
g is open
let g be Function of S,Z; :: thesis: ( f = g & f is open implies g is open )
assume that
A1: f = g and
A2: f is open ; :: thesis: g is open
for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of g . p st R c= g .: P
proof
let p be Point of S; :: thesis: for P being open a_neighborhood of p ex R being a_neighborhood of g . p st R c= g .: P
let P be open a_neighborhood of p; :: thesis: ex R being a_neighborhood of g . p st R c= g .: P
consider R being open a_neighborhood of f . p such that
A3: R c= f .: P by A2, TOPGRP_1:22;
reconsider R2 = R /\ ([#] Z) as Subset of Z ;
reconsider R2 = R2 as a_neighborhood of g . p by A1, Th5;
take R2 ; :: thesis: R2 c= g .: P
R2 c= R by XBOOLE_1:17;
hence R2 c= g .: P by A1, A3; :: thesis: verum
end;
hence g is open by TOPGRP_1:23; :: thesis: verum