consider D1 being set such that
A3: for x being set 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 set 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 set st x in D1 holds
f1 . x = F2(x) from FUNCT_1:sch 3();
 consider D2 being set such that
A7: for x being set 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 set st x in D2 holds
f2 . x = F3(x) from FUNCT_1:sch 3();
 consider D3 being set such that
A10: for x being set 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 set 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 set 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()
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D4 or x in F1() )
thus ( not x in D4 or x in F1() ) by A4; :: thesis: verum
end;
A17: D3 c= F1()
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D3 or x in F1() )
thus ( not x in D3 or x in F1() ) by A10; :: thesis: verum
end;
A18: D2 c= F1()
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D2 or x in F1() )
thus ( not x in D2 or x in F1() ) by A7; :: thesis: verum
end;
D1 c= F1()
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D1 or x in F1() )
thus ( not x in D1 or x in F1() ) by A3; :: thesis: verum
end;
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 set ; :: 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)
then A22: c in D1 by A3, A20;
P3[c] by A1, A20, A21;
then A23: not c in D3 by A10;
P2[c] by A1, A20, A21;
then A24: 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:12
.= (f1 +* f2) . c by A13, A23, FUNCT_4:12
.= f1 . c by A8, A24, FUNCT_4:12
.= F2(c) by A6, A22 ;
:: 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 A25: P2[c] ; :: thesis: (((f1 +* f2) +* f3) +* f4) . c = F3(c)
then A26: c in D2 by A7, A20;
P3[c] by A1, A20, A25;
then A27: not c in D3 by A10;
P4[c] by A1, A20, A25;
then not c in D4 by A4;
hence (((f1 +* f2) +* f3) +* f4) . c = ((f1 +* f2) +* f3) . c by A11, FUNCT_4:12
.= (f1 +* f2) . c by A13, A27, FUNCT_4:12
.= f2 . c by A8, A26, FUNCT_4:14
.= F3(c) by A9, A26 ;
:: thesis: verum
end;
hereby :: thesis: ( P4[c] implies (((f1 +* f2) +* f3) +* f4) . c = F5(c) )
assume A28: P3[c] ; :: thesis: (((f1 +* f2) +* f3) +* f4) . c = F4(c)
then A29: c in D3 by A10, A20;
P4[c] by A1, A20, A28;
then not c in D4 by A4;
hence (((f1 +* f2) +* f3) +* f4) . c = ((f1 +* f2) +* f3) . c by A11, FUNCT_4:12
.= f3 . c by A13, A29, FUNCT_4:14
.= F4(c) by A14, A29 ;
:: thesis: verum
end;
assume P4[c] ; :: thesis: (((f1 +* f2) +* f3) +* f4) . c = F5(c)
then A30: c in D4 by A4, A20;
hence (((f1 +* f2) +* f3) +* f4) . c = f4 . c by A11, FUNCT_4:14
.= F5(c) by A12, A30 ;
:: thesis: verum