let D be non empty set ; :: thesis: for d1, d2 being Element of D

for i being natural Number

for T being Tuple of i,D

for F being BinOp of D st F is associative holds

F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)

let d1, d2 be Element of D; :: thesis: for i being natural Number

for T being Tuple of i,D

for F being BinOp of D st F is associative holds

F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)

let i be natural Number ; :: thesis: for T being Tuple of i,D

for F being BinOp of D st F is associative holds

F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)

let T be Tuple of i,D; :: thesis: for F being BinOp of D st F is associative holds

F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)

let F be BinOp of D; :: thesis: ( F is associative implies F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) )

assume A1: F is associative ; :: thesis: F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)

for i being natural Number

for T being Tuple of i,D

for F being BinOp of D st F is associative holds

F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)

let d1, d2 be Element of D; :: thesis: for i being natural Number

for T being Tuple of i,D

for F being BinOp of D st F is associative holds

F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)

let i be natural Number ; :: thesis: for T being Tuple of i,D

for F being BinOp of D st F is associative holds

F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)

let T be Tuple of i,D; :: thesis: for F being BinOp of D st F is associative holds

F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)

let F be BinOp of D; :: thesis: ( F is associative implies F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2) )

assume A1: F is associative ; :: thesis: F [:] (T,(F . (d1,d2))) = F [:] ((F [:] (T,d1)),d2)