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 :: thesis: for x, y, z being Element of n -tuples_on D holds (product (B,n)) . (((product (B,n)) . (x,y)),z) = (product (B,n)) . (x,((product (B,n)) . (y,z)))

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:28
.= (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 ; :: thesis: verum