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 D3 being set such that
A4: for x being set 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 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 f3 being Function such that
A8: dom f3 = D3 and
A9: for x being set 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 set 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()
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 A4; :: thesis: verum
end;
A14: 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 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 set ; :: 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)
then A18: c in D1 by A3, A16;
P2[c] by A1, A16, A17;
then A19: 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, A19, FUNCT_4:11
.= F2(c) by A6, A18 ;
:: thesis: verum
end;
hereby :: thesis: ( P3[c] implies ((f1 +* f2) +* f3) . c = F4(c) )
assume A20: P2[c] ; :: thesis: ((f1 +* f2) +* f3) . c = F3(c)
then A21: c in D2 by A7, A16;
P3[c] by A1, A16, A20;
then not c in D3 by A4;
hence ((f1 +* f2) +* f3) . c = (f1 +* f2) . c by A8, FUNCT_4:11
.= f2 . c by A10, A21, FUNCT_4:13
.= F3(c) by A11, A21 ;
:: thesis: verum
end;
assume P3[c] ; :: thesis: ((f1 +* f2) +* f3) . c = F4(c)
then A22: c in D3 by A4, A16;
hence ((f1 +* f2) +* f3) . c = f3 . c by A8, FUNCT_4:13
.= F4(c) by A9, A22 ;
:: thesis: verum