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 x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
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 x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
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 x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
let f2 be Function of X2,Y; :: thesis: ( ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) implies for x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) ) )
assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ; :: thesis: for x being Point of X holds
( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
let x be Point of X; :: thesis: ( ( x in the carrier of X1 implies (f1 union f2) . x = f1 . x ) & ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x ) )
set F = f1 union f2;
A2: X1 is SubSpace of X1 union X2 by TSEP_1:22;
hereby :: thesis: ( x in the carrier of X2 implies (f1 union f2) . x = f2 . x )
assume x in the carrier of X1 ; :: thesis: (f1 union f2) . x = f1 . x
hence (f1 union f2) . x = ((f1 union f2) | the carrier of X1) . x by FUNCT_1:49
.= ((f1 union f2) | X1) . x by A2, TMAP_1:def 5
.= f1 . x by A1, TMAP_1:def 12 ;
:: thesis: verum
end;
A3: X2 is SubSpace of X1 union X2 by TSEP_1:22;
assume x in the carrier of X2 ; :: thesis: (f1 union f2) . x = f2 . x
hence (f1 union f2) . x = ((f1 union f2) | the carrier of X2) . x by FUNCT_1:49
.= ((f1 union f2) | X2) . x by A3, TMAP_1:def 5
.= f2 . x by A1, TMAP_1:def 12 ;
:: thesis: verum