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 ) ) )
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 ) )
reconsider Y1 = X1, Y2 = X2, Y3 = X1 union X2 as SubSpace of X1 union X2 by TSEP_1:2, TSEP_1:22;
thus ( X1 is SubSpace of X2 iff f1 union f2 = f2 ) :: thesis: ( X2 is SubSpace of X1 iff f1 union f2 = f1 )

proof

A2: now

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 Def4;
then (f1 union f2) | the carrier of Y3 = f2 by A3;
then (f1 union f2) | (X1 union X2) = f2 by Def4;
hence f1 union f2 = f2 by Th74; :: thesis: verum

end;

now

assume A4: f1 union f2 = f2 ; :: thesis: X1 is SubSpace of X2
A5: dom (f1 union f2) = the carrier of (X1 union X2) by FUNCT_2:def 1;
dom f2 = the carrier of X2 by FUNCT_2:def 1;
then X1 union X2 = TopStruct(# the carrier of X2,the topology of X2 #) by A4, A5, 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: verum

end;

thus ( X2 is SubSpace of X1 iff f1 union f2 = f1 ) :: thesis: verum

proof

A6: now

assume X2 is SubSpace of X1 ; :: thesis: f1 union f2 = f1
then A7: 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 Def4;
then (f1 union f2) | the carrier of Y3 = f1 by A7;
then (f1 union f2) | (X1 union X2) = f1 by Def4;
hence f1 union f2 = f1 by Th74; :: thesis: verum

end;

now

assume A8: f1 union f2 = f1 ; :: thesis: X2 is SubSpace of X1
A9: dom (f1 union f2) = the carrier of (X1 union X2) by FUNCT_2:def 1;
dom f1 = the carrier of X1 by FUNCT_2:def 1;
then X1 union X2 = TopStruct(# the carrier of X1,the topology of X1 #) by A8, A9, 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 A6; :: thesis: verum

end;