let D be non empty set ; :: thesis: for i being natural Number

for T1, T2 being Tuple of i,D

for F being BinOp of D st F is commutative holds

F .: (T1,T2) = F .: (T2,T1)

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

for F being BinOp of D st F is commutative holds

F .: (T1,T2) = F .: (T2,T1)

let T1, T2 be Tuple of i,D; :: thesis: for F being BinOp of D st F is commutative holds

F .: (T1,T2) = F .: (T2,T1)

let F be BinOp of D; :: thesis: ( F is commutative implies F .: (T1,T2) = F .: (T2,T1) )

assume A1: F is commutative ; :: thesis: F .: (T1,T2) = F .: (T2,T1)

for T1, T2 being Tuple of i,D

for F being BinOp of D st F is commutative holds

F .: (T1,T2) = F .: (T2,T1)

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

for F being BinOp of D st F is commutative holds

F .: (T1,T2) = F .: (T2,T1)

let T1, T2 be Tuple of i,D; :: thesis: for F being BinOp of D st F is commutative holds

F .: (T1,T2) = F .: (T2,T1)

let F be BinOp of D; :: thesis: ( F is commutative implies F .: (T1,T2) = F .: (T2,T1) )

assume A1: F is commutative ; :: thesis: F .: (T1,T2) = F .: (T2,T1)