let n be Nat; :: thesis: for D being non empty set
for B being BinOp of D st B is associative holds
product B,n is associative
let D be non empty set ; :: thesis: for B being BinOp of D st B is associative holds
product B,n is associative
let B be BinOp of D; :: thesis: ( B is associative implies product B,n is associative )
assume A1: B is associative ; :: thesis: product B,n is associative

now

let x, y, z be Element of n -tuples_on D; :: thesis: (product B,n) . ((product B,n) . x,y),z = (product B,n) . x,((product B,n) . y,z)
thus (product B,n) . ((product B,n) . x,y),z = (product B,n) . (B .: x,y),z by Def1
.= B .: (B .: x,y),z by Def1
.= B .: x,(B .: y,z) by A1, FINSEQOP:29
.= (product B,n) . x,(B .: y,z) by Def1
.= (product B,n) . x,((product B,n) . y,z) by Def1 ; :: thesis: verum

end;

hence product B,n is associative by BINOP_1:def 3; :: thesis: verum