consider D1 being set such that
A3: for x being object holds
( x in D1 iff ( x in F1() & P1[x] ) ) from XBOOLE_0:sch 1();
 consider D4 being set such that
A4: for x being object holds
( x in D4 iff ( x in F1() & P4[x] ) ) from XBOOLE_0:sch 1();
 consider f1 being Function such that
A5: dom f1 = D1 and
A6: for x being object st x in D1 holds
f1 . x = F2(x) from FUNCT_1:sch 3();
 consider D2 being set such that
A7: for x being object holds
( x in D2 iff ( x in F1() & P2[x] ) ) from XBOOLE_0:sch 1();
 consider f2 being Function such that
A8: dom f2 = D2 and
A9: for x being object st x in D2 holds
f2 . x = F3(x) from FUNCT_1:sch 3();
 consider D3 being set such that
A10: for x being object holds
( x in D3 iff ( x in F1() & P3[x] ) ) from XBOOLE_0:sch 1();
 consider f4 being Function such that
A11: dom f4 = D4 and
A12: for x being object st x in D4 holds
f4 . x = F5(x) from FUNCT_1:sch 3();
 consider f3 being Function such that
A13: dom f3 = D3 and
A14: for x being object st x in D3 holds
f3 . x = F4(x) from FUNCT_1:sch 3();
 set f = ((f1 +* f2) +* f3) +* f4;
take ((f1 +* f2) +* f3) +* f4 ; :: thesis: ( dom (((f1 +* f2) +* f3) +* f4) = F1() & ( for c being set st c in F1() holds
( ( P1[c] implies (((f1 +* f2) +* f3) +* f4) . c = F2(c) ) & ( P2[c] implies (((f1 +* f2) +* f3) +* f4) . c = F3(c) ) & ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) ) ) )
A15: dom (((f1 +* f2) +* f3) +* f4) = (dom ((f1 +* f2) +* f3)) \/ (dom f4) by FUNCT_4:def 1
.= ((dom (f1 +* f2)) \/ (dom f3)) \/ (dom f4) by FUNCT_4:def 1
.= (((dom f1) \/ (dom f2)) \/ (dom f3)) \/ (dom f4) by FUNCT_4:def 1 ;
thus dom (((f1 +* f2) +* f3) +* f4) = F1() :: thesis: for c being set st c in F1() holds
( ( P1[c] implies (((f1 +* f2) +* f3) +* f4) . c = F2(c) ) & ( P2[c] implies (((f1 +* f2) +* f3) +* f4) . c = F3(c) ) & ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) )
proof
A16: D4 c= F1() by A4;
A17: D3 c= F1() by A10;
A18: D2 c= F1() by A7;
D1 c= F1() by A3;
then D1 \/ D2 c= F1() by A18, XBOOLE_1:8;
then (D1 \/ D2) \/ D3 c= F1() by A17, XBOOLE_1:8;
hence dom (((f1 +* f2) +* f3) +* f4) c= F1() by A5, A8, A13, A11, A15, A16, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis: F1() c= dom (((f1 +* f2) +* f3) +* f4)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F1() or x in dom (((f1 +* f2) +* f3) +* f4) )
assume A19: x in F1() ; :: thesis: x in dom (((f1 +* f2) +* f3) +* f4)
then ( P1[x] or P2[x] or P3[x] or P4[x] ) by A2;
then ( x in D1 or x in D2 or x in D3 or x in D4 ) by A3, A7, A10, A4, A19;
then ( x in D1 \/ D2 or x in D3 or x in D4 ) by XBOOLE_0:def 3;
then ( x in (D1 \/ D2) \/ D3 or x in D4 ) by XBOOLE_0:def 3;
hence x in dom (((f1 +* f2) +* f3) +* f4) by A5, A8, A13, A11, A15, XBOOLE_0:def 3; :: thesis: verum
end;
let c be set ; :: thesis: ( c in F1() implies ( ( P1[c] implies (((f1 +* f2) +* f3) +* f4) . c = F2(c) ) & ( P2[c] implies (((f1 +* f2) +* f3) +* f4) . c = F3(c) ) & ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) ) )
assume A20: c in F1() ; :: thesis: ( ( P1[c] implies (((f1 +* f2) +* f3) +* f4) . c = F2(c) ) & ( P2[c] implies (((f1 +* f2) +* f3) +* f4) . c = F3(c) ) & ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) )
hereby :: thesis: ( ( P2[c] implies (((f1 +* f2) +* f3) +* f4) . c = F3(c) ) & ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) )
assume A21: P1[c] ; :: thesis: (((f1 +* f2) +* f3) +* f4) . c = F2(c)
P3[c] by A1, A20, A21;
then A22: not c in D3 by A10;
P2[c] by A1, A20, A21;
then A23: not c in D2 by A7;
P4[c] by A1, A20, A21;
then not c in D4 by A4;
hence (((f1 +* f2) +* f3) +* f4) . c = ((f1 +* f2) +* f3) . c by A11, FUNCT_4:11
.= (f1 +* f2) . c by A13, A22, FUNCT_4:11
.= f1 . c by A8, A23, FUNCT_4:11
.= F2(c) by A6, A21, A3, A20 ;
:: thesis: verum
end;
hereby :: thesis: ( ( P3[c] implies (((f1 +* f2) +* f3) +* f4) . c = F4(c) ) & ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) ) )
assume A24: P2[c] ; :: thesis: (((f1 +* f2) +* f3) +* f4) . c = F3(c)
P3[c] by A1, A20, A24;
then A25: not c in D3 by A10;
P4[c] by A1, A20, A24;
then not c in D4 by A4;
hence (((f1 +* f2) +* f3) +* f4) . c = ((f1 +* f2) +* f3) . c by A11, FUNCT_4:11
.= (f1 +* f2) . c by A13, A25, FUNCT_4:11
.= f2 . c by A8, A24, A7, A20, FUNCT_4:13
.= F3(c) by A9, A24, A7, A20 ;
:: thesis: verum
end;
hereby :: thesis: ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) )
assume A26: P3[c] ; :: thesis: (((f1 +* f2) +* f3) +* f4) . c = F4(c)
P4[c] by A1, A20, A26;
then not c in D4 by A4;
hence (((f1 +* f2) +* f3) +* f4) . c = ((f1 +* f2) +* f3) . c by A11, FUNCT_4:11
.= f3 . c by A13, A26, A10, A20, FUNCT_4:13
.= F4(c) by A14, A26, A10, A20 ;
:: thesis: verum
end;
assume A27: P4[c] ; :: thesis: (((f1 +* f2) +* f3) +* f4) . c = F5(c)
hence (((f1 +* f2) +* f3) +* f4) . c = f4 . c by A11, A4, A20, FUNCT_4:13
.= F5(c) by A12, A27, A4, A20 ;
:: thesis: verum