let A, B be non empty set ; :: thesis: for A1, A2, A3, A12, A23 being non empty Subset of A st A12 = A1 \/ A2 & A23 = A2 \/ A3 holds

for f1 being Function of A1,B

for f2 being Function of A2,B

for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let A1, A2, A3 be non empty Subset of A; :: thesis: for A12, A23 being non empty Subset of A st A12 = A1 \/ A2 & A23 = A2 \/ A3 holds

for f1 being Function of A1,B

for f2 being Function of A2,B

for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let A12, A23 be non empty Subset of A; :: thesis: ( A12 = A1 \/ A2 & A23 = A2 \/ A3 implies for f1 being Function of A1,B

for f2 being Function of A2,B

for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23 )

assume that

A1: A12 = A1 \/ A2 and

A2: A23 = A2 \/ A3 ; :: thesis: for f1 being Function of A1,B

for f2 being Function of A2,B

for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let f1 be Function of A1,B; :: thesis: for f2 being Function of A2,B

for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let f2 be Function of A2,B; :: thesis: for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let f3 be Function of A3,B; :: thesis: ( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) implies for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23 )

assume that

A3: f1 | (A1 /\ A2) = f2 | (A1 /\ A2) and

A4: f2 | (A2 /\ A3) = f3 | (A2 /\ A3) and

A5: f1 | (A1 /\ A3) = f3 | (A1 /\ A3) ; :: thesis: for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let f12 be Function of A12,B; :: thesis: for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let f23 be Function of A23,B; :: thesis: ( f12 = f1 union f2 & f23 = f2 union f3 implies f12 union f3 = f1 union f23 )

assume that

A6: f12 = f1 union f2 and

A7: f23 = f2 union f3 ; :: thesis: f12 union f3 = f1 union f23

A8: (f12 | A2) | (A2 /\ A3) = f2 | (A2 /\ A3) by A3, A6, Def1;

A1 \/ A23 = A12 \/ A3 by A1, A2, XBOOLE_1:4;

then reconsider f = f12 union f3 as Function of (A1 \/ A23),B ;

A12 /\ A3 c= A12 by XBOOLE_1:17;

then reconsider F = f12 | (A12 /\ A3) as Function of (A12 /\ A3),B by FUNCT_2:32;

A9: A2 /\ A3 c= A2 by XBOOLE_1:17;

A10: f12 | A2 = f2 by A3, A6, Def1;

A23 c= A1 \/ A23 by XBOOLE_1:7;

then reconsider H = f | A23 as Function of A23,B by FUNCT_2:32;

A11: A2 c= A12 by A1, XBOOLE_1:7;

A12 /\ A3 c= A3 by XBOOLE_1:17;

then reconsider G = f3 | (A12 /\ A3) as Function of (A12 /\ A3),B by FUNCT_2:32;

A12: A1 /\ A3 c= A1 by XBOOLE_1:17;

A13: (f12 | A1) | (A1 /\ A3) = f1 | (A1 /\ A3) by A3, A6, Def1;

then A22: (f | A12) | A1 = f12 | A1 by Def1;

(f | A12) | A2 = f12 | A2 by A21, Def1;

then A23: f | A2 = f2 by A10, A11, FUNCT_1:51;

A29: A1 c= A12 by A1, XBOOLE_1:7;

f12 | A1 = f1 by A3, A6, Def1;

then f | A1 = f1 by A22, A29, FUNCT_1:51;

hence f12 union f3 = f1 union f23 by A28, Th2; :: thesis: verum

for f1 being Function of A1,B

for f2 being Function of A2,B

for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let A1, A2, A3 be non empty Subset of A; :: thesis: for A12, A23 being non empty Subset of A st A12 = A1 \/ A2 & A23 = A2 \/ A3 holds

for f1 being Function of A1,B

for f2 being Function of A2,B

for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let A12, A23 be non empty Subset of A; :: thesis: ( A12 = A1 \/ A2 & A23 = A2 \/ A3 implies for f1 being Function of A1,B

for f2 being Function of A2,B

for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23 )

assume that

A1: A12 = A1 \/ A2 and

A2: A23 = A2 \/ A3 ; :: thesis: for f1 being Function of A1,B

for f2 being Function of A2,B

for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let f1 be Function of A1,B; :: thesis: for f2 being Function of A2,B

for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let f2 be Function of A2,B; :: thesis: for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds

for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let f3 be Function of A3,B; :: thesis: ( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) implies for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23 )

assume that

A3: f1 | (A1 /\ A2) = f2 | (A1 /\ A2) and

A4: f2 | (A2 /\ A3) = f3 | (A2 /\ A3) and

A5: f1 | (A1 /\ A3) = f3 | (A1 /\ A3) ; :: thesis: for f12 being Function of A12,B

for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let f12 be Function of A12,B; :: thesis: for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds

f12 union f3 = f1 union f23

let f23 be Function of A23,B; :: thesis: ( f12 = f1 union f2 & f23 = f2 union f3 implies f12 union f3 = f1 union f23 )

assume that

A6: f12 = f1 union f2 and

A7: f23 = f2 union f3 ; :: thesis: f12 union f3 = f1 union f23

A8: (f12 | A2) | (A2 /\ A3) = f2 | (A2 /\ A3) by A3, A6, Def1;

A1 \/ A23 = A12 \/ A3 by A1, A2, XBOOLE_1:4;

then reconsider f = f12 union f3 as Function of (A1 \/ A23),B ;

A12 /\ A3 c= A12 by XBOOLE_1:17;

then reconsider F = f12 | (A12 /\ A3) as Function of (A12 /\ A3),B by FUNCT_2:32;

A9: A2 /\ A3 c= A2 by XBOOLE_1:17;

A10: f12 | A2 = f2 by A3, A6, Def1;

A23 c= A1 \/ A23 by XBOOLE_1:7;

then reconsider H = f | A23 as Function of A23,B by FUNCT_2:32;

A11: A2 c= A12 by A1, XBOOLE_1:7;

A12 /\ A3 c= A3 by XBOOLE_1:17;

then reconsider G = f3 | (A12 /\ A3) as Function of (A12 /\ A3),B by FUNCT_2:32;

A12: A1 /\ A3 c= A1 by XBOOLE_1:17;

A13: (f12 | A1) | (A1 /\ A3) = f1 | (A1 /\ A3) by A3, A6, Def1;

now :: thesis: for x being object st x in A12 /\ A3 holds

F . x = G . x

then A21:
f12 | (A12 /\ A3) = f3 | (A12 /\ A3)
by FUNCT_2:12;F . x = G . x

let x be object ; :: thesis: ( x in A12 /\ A3 implies F . x = G . x )

assume A14: x in A12 /\ A3 ; :: thesis: F . x = G . x

A15: A1 /\ A3 c= A12 /\ A3 by A1, XBOOLE_1:7, XBOOLE_1:26;

hence F . x = G . x by A14, A16, A19, XBOOLE_0:def 3; :: thesis: verum

end;assume A14: x in A12 /\ A3 ; :: thesis: F . x = G . x

A15: A1 /\ A3 c= A12 /\ A3 by A1, XBOOLE_1:7, XBOOLE_1:26;

A16: now :: thesis: ( x in A1 /\ A3 implies F . x = G . x )

A18:
A2 /\ A3 c= A12 /\ A3
by A1, XBOOLE_1:7, XBOOLE_1:26;assume A17:
x in A1 /\ A3
; :: thesis: F . x = G . x

hence F . x = (F | (A1 /\ A3)) . x by FUNCT_1:49

.= (f12 | (A1 /\ A3)) . x by A15, FUNCT_1:51

.= (f3 | (A1 /\ A3)) . x by A5, A13, A12, FUNCT_1:51

.= (G | (A1 /\ A3)) . x by A15, FUNCT_1:51

.= G . x by A17, FUNCT_1:49 ;

:: thesis: verum

end;hence F . x = (F | (A1 /\ A3)) . x by FUNCT_1:49

.= (f12 | (A1 /\ A3)) . x by A15, FUNCT_1:51

.= (f3 | (A1 /\ A3)) . x by A5, A13, A12, FUNCT_1:51

.= (G | (A1 /\ A3)) . x by A15, FUNCT_1:51

.= G . x by A17, FUNCT_1:49 ;

:: thesis: verum

A19: now :: thesis: ( x in A2 /\ A3 implies F . x = G . x )

A12 /\ A3 = (A1 /\ A3) \/ (A2 /\ A3)
by A1, XBOOLE_1:23;assume A20:
x in A2 /\ A3
; :: thesis: F . x = G . x

hence F . x = (F | (A2 /\ A3)) . x by FUNCT_1:49

.= (f12 | (A2 /\ A3)) . x by A18, FUNCT_1:51

.= (f3 | (A2 /\ A3)) . x by A4, A8, A9, FUNCT_1:51

.= (G | (A2 /\ A3)) . x by A18, FUNCT_1:51

.= G . x by A20, FUNCT_1:49 ;

:: thesis: verum

end;hence F . x = (F | (A2 /\ A3)) . x by FUNCT_1:49

.= (f12 | (A2 /\ A3)) . x by A18, FUNCT_1:51

.= (f3 | (A2 /\ A3)) . x by A4, A8, A9, FUNCT_1:51

.= (G | (A2 /\ A3)) . x by A18, FUNCT_1:51

.= G . x by A20, FUNCT_1:49 ;

:: thesis: verum

hence F . x = G . x by A14, A16, A19, XBOOLE_0:def 3; :: thesis: verum

then A22: (f | A12) | A1 = f12 | A1 by Def1;

(f | A12) | A2 = f12 | A2 by A21, Def1;

then A23: f | A2 = f2 by A10, A11, FUNCT_1:51;

now :: thesis: for x being object st x in A23 holds

H . x = f23 . x

then A28:
f | A23 = f23
by FUNCT_2:12;H . x = f23 . x

let x be object ; :: thesis: ( x in A23 implies H . x = f23 . x )

assume A24: x in A23 ; :: thesis: H . x = f23 . x

end;assume A24: x in A23 ; :: thesis: H . x = f23 . x

A25: now :: thesis: ( x in A2 implies H . x = f23 . x )

assume A26:
x in A2
; :: thesis: H . x = f23 . x

thus H . x = f . x by A24, FUNCT_1:49

.= f2 . x by A23, A26, FUNCT_1:49

.= (f23 | A2) . x by A4, A7, Def1

.= f23 . x by A26, FUNCT_1:49 ; :: thesis: verum

end;thus H . x = f . x by A24, FUNCT_1:49

.= f2 . x by A23, A26, FUNCT_1:49

.= (f23 | A2) . x by A4, A7, Def1

.= f23 . x by A26, FUNCT_1:49 ; :: thesis: verum

now :: thesis: ( x in A3 implies H . x = f23 . x )

hence
H . x = f23 . x
by A2, A24, A25, XBOOLE_0:def 3; :: thesis: verumassume A27:
x in A3
; :: thesis: H . x = f23 . x

thus H . x = f . x by A24, FUNCT_1:49

.= (f | A3) . x by A27, FUNCT_1:49

.= f3 . x by A21, Def1

.= (f23 | A3) . x by A4, A7, Def1

.= f23 . x by A27, FUNCT_1:49 ; :: thesis: verum

end;thus H . x = f . x by A24, FUNCT_1:49

.= (f | A3) . x by A27, FUNCT_1:49

.= f3 . x by A21, Def1

.= (f23 | A3) . x by A4, A7, Def1

.= f23 . x by A27, FUNCT_1:49 ; :: thesis: verum

A29: A1 c= A12 by A1, XBOOLE_1:7;

f12 | A1 = f1 by A3, A6, Def1;

then f | A1 = f1 by A22, A29, FUNCT_1:51;

hence f12 union f3 = f1 union f23 by A28, Th2; :: thesis: verum