set xy = [:b:] . (x,y);
set yz = [:b:] . (y,z);
let v be object ; :: thesis: ( v in dom a implies ([:b:] . (x,([:b:] . (y,z)))) . v = ([:b:] . (([:b:] . (x,y)),z)) . v )
assume v in dom a ; :: thesis: ([:b:] . (x,([:b:] . (y,z)))) . v = ([:b:] . (([:b:] . (x,y)),z)) . v
then reconsider i = v as Element of dom a ;
A3: ( ([:b:] . (y,z)) . i = (b . i) . ((y . i),(z . i)) & ([:b:] . (x,([:b:] . (y,z)))) . i = (b . i) . ((x . i),(([:b:] . (y,z)) . i)) ) by Def8;
A4: ([:b:] . (([:b:] . (x,y)),z)) . i = (b . i) . ((([:b:] . (x,y)) . i),(z . i)) by Def8;
( b . i is associative & ([:b:] . (x,y)) . i = (b . i) . ((x . i),(y . i)) ) by A1, Def8;
hence ([:b:] . (x,([:b:] . (y,z)))) . v = ([:b:] . (([:b:] . (x,y)),z)) . v by A3, A4; :: thesis: verum