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 object ; :: 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:65;
x is Point of X by PRE_TOPC:25;
then (f1 union f2) . x = f1 . x by A1, A3, Th12;
hence y in f1 .: A by A3, A4, FUNCT_2:35; :: thesis: verum
end;
let y be object ; :: 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 & y = f1 . x ) by FUNCT_2:65;
x is Point of X by PRE_TOPC:25;
then A6: (f1 union f2) . x = f1 . x by A1, Th12;
x in the carrier of (X1 union X2) by A2, XBOOLE_0:def 3;
hence y in (f1 union f2) .: A by A5, A6, FUNCT_2:35; :: 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 object ; :: 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
A7: x in A and
A8: y = (f1 union f2) . x by FUNCT_2:65;
x is Point of X by PRE_TOPC:25;
then (f1 union f2) . x = f2 . x by A1, A7, Th12;
hence y in f2 .: A by A7, A8, FUNCT_2:35; :: thesis: verum
end;
let y be object ; :: 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
A9: ( x in A & y = f2 . x ) by FUNCT_2:65;
x is Point of X by PRE_TOPC:25;
then A10: (f1 union f2) . x = f2 . x by A1, Th12;
x in the carrier of (X1 union X2) by A2, XBOOLE_0:def 3;
hence y in (f1 union f2) .: A by A9, A10, FUNCT_2:35; :: thesis: verum