let f1, f2, f3, f4, g be Function; :: thesis:
assume that
A1: (dom f1) /\ (dom f2) = {} and
A2: (dom f1) /\ (dom f3) = {} and
A3: (dom f1) /\ (dom f4) = {} and
A4: (dom f2) /\ (dom f3) = {} and
A5: (dom f2) /\ (dom f4) = {} and
A6: (dom f3) /\ (dom f4) = {} and
A7: g = ((f1 +* f2) +* f3) +* f4 ; :: thesis:
set f123 = (f1 +* f2) +* f3;
set f12 = f1 +* f2;
thus for x being set st x in dom f1 holds
g . x = f1 . x :: thesis:

let x be set ; :: thesis:
assume A8: x in dom f1 ; :: thesis:
then A9: not x in dom f3 by A2, XBOOLE_0:def 4;
A10: not x in dom f2 by A1, A8, XBOOLE_0:def 4;
not x in dom f4 by A3, A8, XBOOLE_0:def 4;
hence g . x = ((f1 +* f2) +* f3) . x by A7, FUNCT_4:11
.= (f1 +* f2) . x by A9, FUNCT_4:11
.= f1 . x by A10, FUNCT_4:11 ;
:: thesis:

end;

thus for x being set st x in dom f2 holds
g . x = f2 . x :: thesis:

let x be set ; :: thesis:
assume A11: x in dom f2 ; :: thesis:
then A12: not x in dom f3 by A4, XBOOLE_0:def 4;
not x in dom f4 by A5, A11, XBOOLE_0:def 4;
hence g . x = ((f1 +* f2) +* f3) . x by A7, FUNCT_4:11
.= (f1 +* f2) . x by A12, FUNCT_4:11
.= f2 . x by A11, FUNCT_4:13 ;
:: thesis:

end;

thus for x being set st x in dom f3 holds
g . x = f3 . x :: thesis:

let x be set ; :: thesis:
assume A13: x in dom f3 ; :: thesis:
then not x in dom f4 by A6, XBOOLE_0:def 4;
hence g . x = ((f1 +* f2) +* f3) . x by A7, FUNCT_4:11
.= f3 . x by A13, FUNCT_4:13 ;
:: thesis:

end;

thus for x being set st x in dom f4 holds
g . x = f4 . x by A7, FUNCT_4:13; :: thesis: