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 b₁ being continuous Function of (Top2NTop TX),(Top2NTop TY) holds
( b₁ = Top2NTop f iff b₁ = f ) ) ) by Lm27; :: thesis: verum