let X, Y be non empty TopSpace; 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; 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; 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; ( ( 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) )
; ( ( 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;
let A be Subset of X2; (f1 union f2) .: A = f2 .: A
let y be object ; TARSKI:def 3 ( not y in f2 .: A or y in (f1 union f2) .: A )
assume
y in f2 .: A
; 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; verum