let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C holds (f ++ g) ++ h = f ++ (g ++ h)
let f, h, g be Membership_Func of C; :: thesis: (f ++ g) ++ h = f ++ (g ++ h)
A1: C = dom (f ++ (g ++ h)) by FUNCT_2:def 1;
A2: for c being Element of C st c in C holds
((f ++ g) ++ h) . c = (f ++ (g ++ h)) . c

proof

let c be Element of C; :: thesis: ( c in C implies ((f ++ g) ++ h) . c = (f ++ (g ++ h)) . c )
set x = f . c;
set y = g . c;
set z = h . c;
A3: (f ++ (g ++ h)) . c = ((f . c) + ((g ++ h) . c)) - ((f . c) * ((g ++ h) . c)) by Def3
.= ((f . c) + (((g . c) + (h . c)) - ((g . c) * (h . c)))) - ((f . c) * ((g ++ h) . c)) by Def3
.= (((f . c) + ((g . c) + (h . c))) - ((g . c) * (h . c))) - ((f . c) * (((g . c) + (h . c)) - ((g . c) * (h . c)))) by Def3
.= ((((- ((g . c) * (h . c))) - ((f . c) * (g . c))) - ((f . c) * (h . c))) + (((f . c) * (g . c)) * (h . c))) + (((f . c) + (g . c)) + (h . c)) ;
((f ++ g) ++ h) . c = (((f ++ g) . c) + (h . c)) - (((f ++ g) . c) * (h . c)) by Def3
.= ((((f . c) + (g . c)) - ((f . c) * (g . c))) + (h . c)) - (((f ++ g) . c) * (h . c)) by Def3
.= (((- ((f . c) * (g . c))) + ((f . c) + (g . c))) + (h . c)) - ((((f . c) + (g . c)) - ((f . c) * (g . c))) * (h . c)) by Def3
.= ((((- ((f . c) * (g . c))) - ((f . c) * (h . c))) - ((g . c) * (h . c))) + (((f . c) * (g . c)) * (h . c))) + (((f . c) + (g . c)) + (h . c)) ;
hence ( c in C implies ((f ++ g) ++ h) . c = (f ++ (g ++ h)) . c ) by A3; :: thesis: verum

end;

C = dom ((f ++ g) ++ h) by FUNCT_2:def 1;
hence (f ++ g) ++ h = f ++ (g ++ h) by A1, A2, PARTFUN1:5; :: thesis: verum