now :: thesis: for a, b, c being Element of D holds (D -pr1) . (a,((D -pr1) . (b,c))) = (D -pr1) . (((D -pr1) . (a,b)),c)

let a, b, c be Element of D; :: thesis: (D -pr1) . (a,((D -pr1) . (b,c))) = (D -pr1) . (((D -pr1) . (a,b)),c)
( (D -pr1) . (a,((D -pr1) . (b,c))) = a & (D -pr1) . (((D -pr1) . (a,b)),c) = (D -pr1) . (a,c) ) by FUNCT_3:def 4;
hence (D -pr1) . (a,((D -pr1) . (b,c))) = (D -pr1) . (((D -pr1) . (a,b)),c) by FUNCT_3:def 4; :: thesis: verum

end;

hence for b₁ being BinOp of D st b₁ = D -pr1 holds
b₁ is associative ; :: thesis: verum