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

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)))

hence
product (B,n) is associative
; :: thesis: verumlet 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;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