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