let X, Y be non empty TopSpace; :: thesis: for X1, X2, X3 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y
for f3 being Function of X3,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) & ( X1 misses X3 or f1 | (X1 meet X3) = f3 | (X1 meet X3) ) & ( X2 misses X3 or f2 | (X2 meet X3) = f3 | (X2 meet X3) ) holds
(f1 union f2) union f3 = f1 union (f2 union f3)

let X1, X2, X3 be non empty SubSpace of X; :: thesis: for f1 being Function of X1,Y
for f2 being Function of X2,Y
for f3 being Function of X3,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) & ( X1 misses X3 or f1 | (X1 meet X3) = f3 | (X1 meet X3) ) & ( X2 misses X3 or f2 | (X2 meet X3) = f3 | (X2 meet X3) ) holds
(f1 union f2) union f3 = f1 union (f2 union f3)

let f1 be Function of X1,Y; :: thesis: for f2 being Function of X2,Y
for f3 being Function of X3,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) & ( X1 misses X3 or f1 | (X1 meet X3) = f3 | (X1 meet X3) ) & ( X2 misses X3 or f2 | (X2 meet X3) = f3 | (X2 meet X3) ) holds
(f1 union f2) union f3 = f1 union (f2 union f3)

let f2 be Function of X2,Y; :: thesis: for f3 being Function of X3,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) & ( X1 misses X3 or f1 | (X1 meet X3) = f3 | (X1 meet X3) ) & ( X2 misses X3 or f2 | (X2 meet X3) = f3 | (X2 meet X3) ) holds
(f1 union f2) union f3 = f1 union (f2 union f3)

let f3 be Function of X3,Y; :: thesis: ( ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) & ( X1 misses X3 or f1 | (X1 meet X3) = f3 | (X1 meet X3) ) & ( X2 misses X3 or f2 | (X2 meet X3) = f3 | (X2 meet X3) ) implies (f1 union f2) union f3 = f1 union (f2 union f3) )
assume that
A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) and
A2: ( X1 misses X3 or f1 | (X1 meet X3) = f3 | (X1 meet X3) ) and
A3: ( X2 misses X3 or f2 | (X2 meet X3) = f3 | (X2 meet X3) ) ; :: thesis: (f1 union f2) union f3 = f1 union (f2 union f3)
set g = (f1 union f2) union f3;
A4: (X1 union X2) union X3 = X1 union (X2 union X3) by TSEP_1:21;
then reconsider f = (f1 union f2) union f3 as Function of (X1 union (X2 union X3)),Y ;
A5: X1 union X2 is SubSpace of X1 union (X2 union X3) by ;
A6: now :: thesis: ( X1 union X2 meets X3 implies (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3) )
assume A7: X1 union X2 meets X3 ; :: thesis: (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3)
now :: thesis: (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3)
per cases ( ( X1 meets X3 & not X2 meets X3 ) or ( not X1 meets X3 & X2 meets X3 ) or ( X1 meets X3 & X2 meets X3 ) ) by ;
suppose A8: ( X1 meets X3 & not X2 meets X3 ) ; :: thesis: (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3)
then A9: (X1 union X2) meet X3 = X1 meet X3 by Th26;
A10: X1 is SubSpace of X1 union X2 by TSEP_1:22;
X1 meet X3 is SubSpace of X1 by ;
then (f1 union f2) | (X1 meet X3) = ((f1 union f2) | X1) | (X1 meet X3) by
.= f1 | (X1 meet X3) by ;
hence (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3) by A2, A8, A9; :: thesis: verum
end;
suppose A11: ( not X1 meets X3 & X2 meets X3 ) ; :: thesis: (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3)
then A12: (X1 union X2) meet X3 = X2 meet X3 by Th26;
A13: X2 is SubSpace of X1 union X2 by TSEP_1:22;
X2 meet X3 is SubSpace of X2 by ;
then (f1 union f2) | (X2 meet X3) = ((f1 union f2) | X2) | (X2 meet X3) by
.= f2 | (X2 meet X3) by ;
hence (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3) by A3, A11, A12; :: thesis: verum
end;
suppose A14: ( X1 meets X3 & X2 meets X3 ) ; :: thesis: (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3)
then ( X1 meet X3 is SubSpace of X3 & X2 meet X3 is SubSpace of X3 ) by TSEP_1:27;
then A15: (X1 meet X3) union (X2 meet X3) is SubSpace of X3 by Th24;
A16: X2 meet X3 is SubSpace of X2 by ;
A17: X1 meet X3 is SubSpace of (X1 meet X3) union (X2 meet X3) by TSEP_1:22;
then A18: (f3 | ((X1 meet X3) union (X2 meet X3))) | (X1 meet X3) = f3 | (X1 meet X3) by ;
A19: X1 meet X3 is SubSpace of X1 by ;
then A20: (X1 meet X3) union (X2 meet X3) is SubSpace of X1 union X2 by ;
then A21: ((f1 union f2) | ((X1 meet X3) union (X2 meet X3))) | (X1 meet X3) = (f1 union f2) | (X1 meet X3) by ;
X2 is SubSpace of X1 union X2 by TSEP_1:22;
then A22: (f1 union f2) | (X2 meet X3) = ((f1 union f2) | X2) | (X2 meet X3) by
.= f2 | (X2 meet X3) by ;
set v = f3 | ((X1 meet X3) union (X2 meet X3));
A23: X2 meet X3 is SubSpace of (X1 meet X3) union (X2 meet X3) by TSEP_1:22;
then A24: (f3 | ((X1 meet X3) union (X2 meet X3))) | (X2 meet X3) = f3 | (X2 meet X3) by ;
X1 is SubSpace of X1 union X2 by TSEP_1:22;
then A25: (f1 union f2) | (X1 meet X3) = ((f1 union f2) | X1) | (X1 meet X3) by
.= f1 | (X1 meet X3) by ;
A26: ((f1 union f2) | ((X1 meet X3) union (X2 meet X3))) | (X2 meet X3) = (f1 union f2) | (X2 meet X3) by ;
(f1 union f2) | ((X1 union X2) meet X3) = (f1 union f2) | ((X1 meet X3) union (X2 meet X3)) by
.= ((f3 | ((X1 meet X3) union (X2 meet X3))) | (X1 meet X3)) union ((f3 | ((X1 meet X3) union (X2 meet X3))) | (X2 meet X3)) by A2, A3, A14, A25, A22, A21, A26, A18, A24, Th126
.= f3 | ((X1 meet X3) union (X2 meet X3)) by Th126 ;
hence (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3) by ; :: thesis: verum
end;
end;
end;
hence (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3) ; :: thesis: verum
end;
then ( X1 union X2 is SubSpace of (X1 union X2) union X3 & ((f1 union f2) union f3) | (X1 union X2) = f1 union f2 ) by ;
then A27: f | the carrier of (X1 union X2) = f1 union f2 by Def5;
A28: X3 is SubSpace of X1 union (X2 union X3) by ;
A29: X2 union X3 is SubSpace of X1 union (X2 union X3) by TSEP_1:22;
( X3 is SubSpace of (X1 union X2) union X3 & ((f1 union f2) union f3) | X3 = f3 ) by ;
then A30: f | the carrier of X3 = f3 by Def5;
A31: X1 union X2 is SubSpace of X1 union (X2 union X3) by ;
X3 is SubSpace of X2 union X3 by TSEP_1:22;
then A32: (f | (X2 union X3)) | X3 = f | X3 by
.= f3 by ;
X2 is SubSpace of X1 union X2 by TSEP_1:22;
then A33: f | X2 = (f | (X1 union X2)) | X2 by
.= (f1 union f2) | X2 by ;
X2 is SubSpace of X2 union X3 by TSEP_1:22;
then (f | (X2 union X3)) | X2 = f | X2 by
.= f2 by ;
then A34: f | (X2 union X3) = f2 union f3 by ;
X1 is SubSpace of X1 union X2 by TSEP_1:22;
then f | X1 = (f | (X1 union X2)) | X1 by
.= (f1 union f2) | X1 by ;
then f | X1 = f1 by ;
hence (f1 union f2) union f3 = f1 union (f2 union f3) by ; :: thesis: verum