let D be non empty set ; :: thesis: for d being Element of D

for F being BinOp of D

for i, j being Nat st F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds

F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))

let d be Element of D; :: thesis: for F being BinOp of D

for i, j being Nat st F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds

F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))

let F be BinOp of D; :: thesis: for i, j being Nat st F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds

F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))

let i, j be Nat; :: thesis: ( F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) implies F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) )

assume that

A1: ( F is commutative & F is associative ) and

A2: ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) ; :: thesis: F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))

for F being BinOp of D

for i, j being Nat st F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds

F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))

let d be Element of D; :: thesis: for F being BinOp of D

for i, j being Nat st F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds

F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))

let F be BinOp of D; :: thesis: for i, j being Nat st F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) holds

F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))

let i, j be Nat; :: thesis: ( F is commutative & F is associative & ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) implies F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) )

assume that

A1: ( F is commutative & F is associative ) and

A2: ( ( i >= 1 & j >= 1 ) or F is having_a_unity ) ; :: thesis: F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))

per cases
( i = 0 or j = 0 or ( i > 0 & j > 0 ) )
;

end;

suppose A3:
( i = 0 or j = 0 )
; :: thesis: F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))

set e = the_unity_wrt F;

hence F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) by A2, A3, A4, FINSOP_1:10; :: thesis: verum

end;A4: now :: thesis: F "**" (j |-> (F "**" (i |-> d))) = the_unity_wrt F

(i * j) |-> d = <*> D
by A3;end;

hence F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) by A2, A3, A4, FINSOP_1:10; :: thesis: verum

suppose A5:
( i > 0 & j > 0 )
; :: thesis: F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d)))

defpred S_{1}[ Nat] means ( $1 <> 0 implies F "**" ((i * $1) |-> d) = F "**" ($1 |-> (F "**" (i |-> d))) );

A6: for j being Nat st S_{1}[j] holds

S_{1}[j + 1]
_{1}[ 0 ]
;

for j being Nat holds S_{1}[j]
from NAT_1:sch 2(A11, A6);

hence F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) by A5; :: thesis: verum

end;A6: for j being Nat st S

S

proof

A11:
S
let j be Nat; :: thesis: ( S_{1}[j] implies S_{1}[j + 1] )

assume A7: ( j <> 0 implies F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) ) ; :: thesis: S_{1}[j + 1]

_{1}[j + 1]
; :: thesis: verum

end;assume A7: ( j <> 0 implies F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) ) ; :: thesis: S

now :: thesis: S_{1}[j + 1]end;

hence
Sper cases
( j = 0 or j >= 1 + 0 )
by NAT_1:14;

end;

suppose A8:
j = 0
; :: thesis: S_{1}[j + 1]

1 |-> (F "**" (i |-> d)) = <*(F "**" (i |-> d))*>
by FINSEQ_2:59;

hence S_{1}[j + 1]
by A8, FINSOP_1:11; :: thesis: verum

end;hence S

suppose A9:
j >= 1 + 0
; :: thesis: S_{1}[j + 1]

then
j > 0
;

then i * j > i * 0 by A5, XREAL_1:68;

then A10: i * j >= 1 + 0 by NAT_1:13;

F "**" ((i * (j + 1)) |-> d) = F "**" (((i * j) + (i * 1)) |-> d)

.= F . ((F "**" ((i * j) |-> d)),(F "**" (i |-> d))) by A1, A2, A10, Th26

.= F . ((F "**" ((i * j) |-> d)),(F "**" (1 |-> (F "**" (i |-> d))))) by FINSOP_1:16

.= F "**" ((j + 1) |-> (F "**" (i |-> d))) by A1, A7, A9, Th26 ;

hence S_{1}[j + 1]
; :: thesis: verum

end;then i * j > i * 0 by A5, XREAL_1:68;

then A10: i * j >= 1 + 0 by NAT_1:13;

F "**" ((i * (j + 1)) |-> d) = F "**" (((i * j) + (i * 1)) |-> d)

.= F . ((F "**" ((i * j) |-> d)),(F "**" (i |-> d))) by A1, A2, A10, Th26

.= F . ((F "**" ((i * j) |-> d)),(F "**" (1 |-> (F "**" (i |-> d))))) by FINSOP_1:16

.= F "**" ((j + 1) |-> (F "**" (i |-> d))) by A1, A7, A9, Th26 ;

hence S

for j being Nat holds S

hence F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) by A5; :: thesis: verum