let X, Y be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X

for g being Function of X0,Y ex h being Function of X,Y st h | X0 = g

let X0 be non empty SubSpace of X; :: thesis: for g being Function of X0,Y ex h being Function of X,Y st h | X0 = g

let g be Function of X0,Y; :: thesis: ex h being Function of X,Y st h | X0 = g

for g being Function of X0,Y ex h being Function of X,Y st h | X0 = g

let X0 be non empty SubSpace of X; :: thesis: for g being Function of X0,Y ex h being Function of X,Y st h | X0 = g

let g be Function of X0,Y; :: thesis: ex h being Function of X,Y st h | X0 = g

now :: thesis: ex h being Function of X,Y st h | X0 = gend;

hence
ex h being Function of X,Y st h | X0 = g
; :: thesis: verumper cases
( TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X0, the topology of X0 #) or TopStruct(# the carrier of X, the topology of X #) <> TopStruct(# the carrier of X0, the topology of X0 #) )
;

end;

suppose A1:
TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X0, the topology of X0 #)
; :: thesis: ex h being Function of X,Y st h | X0 = g

then reconsider h = g as Function of X,Y ;

take h = h; :: thesis: h | X0 = g

thus h | X0 = g by A1, Th54; :: thesis: verum

end;take h = h; :: thesis: h | X0 = g

thus h | X0 = g by A1, Th54; :: thesis: verum

suppose A2:
TopStruct(# the carrier of X, the topology of X #) <> TopStruct(# the carrier of X0, the topology of X0 #)
; :: thesis: ex h being Function of X,Y st h | X0 = g

Y is SubSpace of Y
by TSEP_1:2;

then reconsider B = the carrier of Y as non empty Subset of Y by TSEP_1:1;

set y = the Element of B;

reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;

A3: X is SubSpace of X by TSEP_1:2;

then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1;

reconsider A1 = A \ A0 as Subset of X ;

A4: A0 misses A1 by XBOOLE_1:79;

A0 <> A by A2, A3, TSEP_1:5;

then reconsider A1 = A1 as non empty Subset of A by XBOOLE_1:37;

reconsider g1 = A1 --> the Element of B as Function of A1,B ;

reconsider A0 = A0 as non empty Subset of A ;

reconsider g0 = g as Function of A0,B ;

set G = g0 union g1;

the carrier of X = A1 \/ A0 by XBOOLE_1:45;

then reconsider h = g0 union g1 as Function of X,Y ;

take h = h; :: thesis: h | X0 = g

thus h | X0 = g by A4, Th1; :: thesis: verum

end;then reconsider B = the carrier of Y as non empty Subset of Y by TSEP_1:1;

set y = the Element of B;

reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;

A3: X is SubSpace of X by TSEP_1:2;

then reconsider A = the carrier of X as non empty Subset of X by TSEP_1:1;

reconsider A1 = A \ A0 as Subset of X ;

A4: A0 misses A1 by XBOOLE_1:79;

A0 <> A by A2, A3, TSEP_1:5;

then reconsider A1 = A1 as non empty Subset of A by XBOOLE_1:37;

reconsider g1 = A1 --> the Element of B as Function of A1,B ;

reconsider A0 = A0 as non empty Subset of A ;

reconsider g0 = g as Function of A0,B ;

set G = g0 union g1;

the carrier of X = A1 \/ A0 by XBOOLE_1:45;

then reconsider h = g0 union g1 as Function of X,Y ;

take h = h; :: thesis: h | X0 = g

thus h | X0 = g by A4, Th1; :: thesis: verum