let X, Y be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) holds
( ( X1 is SubSpace of X2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies X1 is SubSpace of X2 ) & ( X2 is SubSpace of X1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies X2 is SubSpace of X1 ) )
let X1, X2 be non empty SubSpace of X; :: thesis: for f1 being Function of X1,Y
for f2 being Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) holds
( ( X1 is SubSpace of X2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies X1 is SubSpace of X2 ) & ( X2 is SubSpace of X1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies X2 is SubSpace of X1 ) )
let f1 be Function of X1,Y; :: thesis: for f2 being Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) holds
( ( X1 is SubSpace of X2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies X1 is SubSpace of X2 ) & ( X2 is SubSpace of X1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies X2 is SubSpace of X1 ) )
let f2 be Function of X2,Y; :: thesis: ( f1 | (X1 meet X2) = f2 | (X1 meet X2) implies ( ( X1 is SubSpace of X2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies X1 is SubSpace of X2 ) & ( X2 is SubSpace of X1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies X2 is SubSpace of X1 ) ) )
reconsider Y1 = X1, Y2 = X2, Y3 = X1 union X2 as SubSpace of X1 union X2 by TSEP_1:2, TSEP_1:22;
assume A1: f1 | (X1 meet X2) = f2 | (X1 meet X2) ; :: thesis: ( ( X1 is SubSpace of X2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies X1 is SubSpace of X2 ) & ( X2 is SubSpace of X1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies X2 is SubSpace of X1 ) )

A2: now :: thesis: ( X1 is SubSpace of X2 implies f1 union f2 = f2 )

assume X1 is SubSpace of X2 ; :: thesis: f1 union f2 = f2
then A3: TopStruct(# the carrier of X2, the topology of X2 #) = X1 union X2 by TSEP_1:23;
(f1 union f2) | X2 = f2 by A1, Def12;
then (f1 union f2) | the carrier of Y2 = f2 by Def5;
then (f1 union f2) | the carrier of Y3 = f2 by A3;
then (f1 union f2) | (X1 union X2) = f2 by Def5;
hence f1 union f2 = f2 by Th67; :: thesis: verum

end;

A4: now :: thesis: ( X2 is SubSpace of X1 implies f1 union f2 = f1 )

assume X2 is SubSpace of X1 ; :: thesis: f1 union f2 = f1
then A5: TopStruct(# the carrier of X1, the topology of X1 #) = X1 union X2 by TSEP_1:23;
(f1 union f2) | X1 = f1 by A1, Def12;
then (f1 union f2) | the carrier of Y1 = f1 by Def5;
then (f1 union f2) | the carrier of Y3 = f1 by A5;
then (f1 union f2) | (X1 union X2) = f1 by Def5;
hence f1 union f2 = f1 by Th67; :: thesis: verum

end;

now :: thesis: ( f1 union f2 = f2 implies X1 is SubSpace of X2 )

A6: ( dom (f1 union f2) = the carrier of (X1 union X2) & dom f2 = the carrier of X2 ) by FUNCT_2:def 1;
assume f1 union f2 = f2 ; :: thesis: X1 is SubSpace of X2
then X1 union X2 = TopStruct(# the carrier of X2, the topology of X2 #) by A6, TSEP_1:5;
hence X1 is SubSpace of X2 by TSEP_1:23; :: thesis: verum

end;

hence ( X1 is SubSpace of X2 iff f1 union f2 = f2 ) by A2; :: thesis: ( X2 is SubSpace of X1 iff f1 union f2 = f1 )

now :: thesis: ( f1 union f2 = f1 implies X2 is SubSpace of X1 )

A7: ( dom (f1 union f2) = the carrier of (X1 union X2) & dom f1 = the carrier of X1 ) by FUNCT_2:def 1;
assume f1 union f2 = f1 ; :: thesis: X2 is SubSpace of X1
then X1 union X2 = TopStruct(# the carrier of X1, the topology of X1 #) by A7, TSEP_1:5;
hence X2 is SubSpace of X1 by TSEP_1:23; :: thesis: verum

end;

hence ( X2 is SubSpace of X1 iff f1 union f2 = f1 ) by A4; :: thesis: verum