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
now :: thesis: ex h being Function of X,Y st h | X0 = g
per 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 #) ) ;
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;
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;
end;
end;
hence ex h being Function of X,Y st h | X0 = g ; :: thesis: verum