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 A4, TSEP_1:22;
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 A7, Th34;
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 A8, TSEP_1:27;
then (f1 union f2) | (X1 meet X3) = ((f1 union f2) | X1) | (X1 meet X3) by A10, Th72
.= f1 | (X1 meet X3) by A1, Def12 ;
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 A11, TSEP_1:27;
then (f1 union f2) | (X2 meet X3) = ((f1 union f2) | X2) | (X2 meet X3) by A13, Th72
.= f2 | (X2 meet X3) by A1, Def12 ;
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 A14, TSEP_1:27;
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 A15, Th72;
A19: X1 meet X3 is SubSpace of X1 by A14, TSEP_1:27;
then A20: (X1 meet X3) union (X2 meet X3) is SubSpace of X1 union X2 by A16, Th22;
then A21: ((f1 union f2) | ((X1 meet X3) union (X2 meet X3))) | (X1 meet X3) = (f1 union f2) | (X1 meet X3) by A17, Th72;
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 A16, Th72
.= f2 | (X2 meet X3) by A1, Def12 ;
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 A15, Th72;
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 A19, Th72
.= f1 | (X1 meet X3) by A1, Def12 ;
A26: ((f1 union f2) | ((X1 meet X3) union (X2 meet X3))) | (X2 meet X3) = (f1 union f2) | (X2 meet X3) by A20, A23, Th72;
(f1 union f2) | ((X1 union X2) meet X3) = (f1 union f2) | ((X1 meet X3) union (X2 meet X3)) by A14, TSEP_1:32
.= ((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 A14, TSEP_1:32; :: 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 Def12, TSEP_1:22;
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 A4, TSEP_1:22;
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 A6, Def12, TSEP_1:22;
then A30: f | the carrier of X3 = f3 by Def5;
A31: X1 union X2 is SubSpace of X1 union (X2 union X3) by A4, TSEP_1:22;
X3 is SubSpace of X2 union X3 by TSEP_1:22;
then A32: (f | (X2 union X3)) | X3 = f | X3 by A29, Th72
.= f3 by A28, A30, Def5 ;
X2 is SubSpace of X1 union X2 by TSEP_1:22;
then A33: f | X2 = (f | (X1 union X2)) | X2 by A31, Th72
.= (f1 union f2) | X2 by A5, A27, Def5 ;
X2 is SubSpace of X2 union X3 by TSEP_1:22;
then (f | (X2 union X3)) | X2 = f | X2 by A29, Th72
.= f2 by A1, A33, Def12 ;
then A34: f | (X2 union X3) = f2 union f3 by A32, Th126;
X1 is SubSpace of X1 union X2 by TSEP_1:22;
then f | X1 = (f | (X1 union X2)) | X1 by A31, Th72
.= (f1 union f2) | X1 by A5, A27, Def5 ;
then f | X1 = f1 by A1, Def12;
hence (f1 union f2) union f3 = f1 union (f2 union f3) by A34, Th126; :: thesis: verum