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

hence (f * g) * h = f * (g * h) by A1, A2, PARTFUN1:5; :: thesis: verum

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

C = dom ((f * g) * h)
by FUNCT_2:def 1;
let c be Element of C; :: thesis: ( c in C implies ((f * g) * h) . c = (f * (g * h)) . c )

((f * g) * h) . c = ((f * g) . c) * (h . c) by Def2

.= ((f . c) * (g . c)) * (h . c) by Def2

.= (f . c) * ((g . c) * (h . c))

.= (f . c) * ((g * h) . c) by Def2 ;

hence ( c in C implies ((f * g) * h) . c = (f * (g * h)) . c ) by Def2; :: thesis: verum

end;((f * g) * h) . c = ((f * g) . c) * (h . c) by Def2

.= ((f . c) * (g . c)) * (h . c) by Def2

.= (f . c) * ((g . c) * (h . c))

.= (f . c) * ((g * h) . c) by Def2 ;

hence ( c in C implies ((f * g) * h) . c = (f * (g * h)) . c ) by Def2; :: thesis: verum

hence (f * g) * h = f * (g * h) by A1, A2, PARTFUN1:5; :: thesis: verum