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 ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) )
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 ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) )
let f1 be Function of X1,Y; :: thesis: for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) )
let f2 be Function of X2,Y; :: thesis: ( ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) implies ( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) ) )
assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ; :: thesis: ( ( for A being Subset of X1 holds (f1 union f2) .: A = f1 .: A ) & ( for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A ) )
set F = f1 union f2;
A2: the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def 2;

hereby :: thesis: for A being Subset of X2 holds (f1 union f2) .: A = f2 .: A

let A be Subset of X1; :: thesis: (f1 union f2) .: A = f1 .: A
thus (f1 union f2) .: A = f1 .: A :: thesis: verum

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: f1 .: A c= (f1 union f2) .: A

let y be set ; :: thesis: ( y in (f1 union f2) .: A implies y in f1 .: A )
assume y in (f1 union f2) .: A ; :: thesis: y in f1 .: A
then consider x being Element of (X1 union X2) such that
A3: x in A and
A4: y = (f1 union f2) . x by FUNCT_2:116;
x is Point of X by PRE_TOPC:55;
then (f1 union f2) . x = f1 . x by A1, A3, Th14;
hence y in f1 .: A by A3, A4, FUNCT_2:43; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f1 .: A or y in (f1 union f2) .: A )
assume y in f1 .: A ; :: thesis: y in (f1 union f2) .: A
then consider x being Element of X1 such that
A5: x in A and
A6: y = f1 . x by FUNCT_2:116;
x is Point of X by PRE_TOPC:55;
then A7: (f1 union f2) . x = f1 . x by A1, Th14;
x in the carrier of (X1 union X2) by A2, XBOOLE_0:def 3;
hence y in (f1 union f2) .: A by A5, A6, A7, FUNCT_2:43; :: thesis: verum

end;

end;

let A be Subset of X2; :: thesis: (f1 union f2) .: A = f2 .: A

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: f2 .: A c= (f1 union f2) .: A

let y be set ; :: thesis: ( y in (f1 union f2) .: A implies y in f2 .: A )
assume y in (f1 union f2) .: A ; :: thesis: y in f2 .: A
then consider x being Element of (X1 union X2) such that
A8: x in A and
A9: y = (f1 union f2) . x by FUNCT_2:116;
x is Point of X by PRE_TOPC:55;
then (f1 union f2) . x = f2 . x by A1, A8, Th14;
hence y in f2 .: A by A8, A9, FUNCT_2:43; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in f2 .: A or y in (f1 union f2) .: A )
assume y in f2 .: A ; :: thesis: y in (f1 union f2) .: A
then consider x being Element of X2 such that
A10: x in A and
A11: y = f2 . x by FUNCT_2:116;
x is Point of X by PRE_TOPC:55;
then A12: (f1 union f2) . x = f2 . x by A1, Th14;
x in the carrier of (X1 union X2) by A2, XBOOLE_0:def 3;
hence y in (f1 union f2) .: A by A10, A11, A12, FUNCT_2:43; :: thesis: verum