set NTX = Top2NTop TX;
set NTY = Top2NTop TY;
reconsider f9 = Top2NTop f as Function of (Top2NTop TX),(Top2NTop TY) ;
now :: thesis: for F being closed Subset of (Top2NTop TY) holds f9 " F is closed Subset of (Top2NTop TX)
let F be closed Subset of (Top2NTop TY); :: thesis: f9 " F is closed Subset of (Top2NTop TX)
reconsider F9 = F as closed Subset of (NTop2Top (Top2NTop TY)) by Lm10;
reconsider TY9 = TY as non empty TopSpace ;
NTop2Top (Top2NTop TY) = TY9 by FINTOPO7:24;
then reconsider F9 = F9 as closed Subset of TY ;
f " F9 is closed Subset of TX by PRE_TOPC:def 6;
hence f9 " F is closed Subset of (Top2NTop TX) by Lm7; :: thesis: verum
end;
hence ( Top2NTop f is continuous Function of (Top2NTop TX),(Top2NTop TY) & ( for b1 being continuous Function of (Top2NTop TX),(Top2NTop TY) holds
( b1 = Top2NTop f iff b1 = f ) ) ) by Lm27; :: thesis: verum