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;

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

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) )

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;assume A7:
X1 union X2 meets X3
; :: thesis: (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3)

end;now :: thesis: (f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3)end;

hence
(f1 union f2) | ((X1 union X2) meet X3) = f3 | ((X1 union X2) meet X3)
; :: thesis: verumper 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;

end;

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;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

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;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

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;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

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