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
f1 union f2 = f2 union f1
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
f1 union f2 = f2 union f1
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
f1 union f2 = f2 union f1
let f2 be Function of X2,Y; :: thesis: ( ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) implies f1 union f2 = f2 union f1 )
assume ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ; :: thesis: f1 union f2 = f2 union f1
then ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) by Def12;
hence f1 union f2 = f2 union f1 by Th126; :: thesis: verum