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

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

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

set e = the_unity_wrt F;

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

per cases ( i = 0 or j = 0 ) by A3;

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

then i |-> d = <*> D ;
then F "**" (i |-> d) = the_unity_wrt F by A2, A3, FINSOP_1:10;
hence F "**" (j |-> (F "**" (i |-> d))) = the_unity_wrt F by A2, A3, Th25; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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

defpred S₁[ Nat] means ( $1 <> 0 implies F "**" ((i * $1) |-> d) = F "**" ($1 |-> (F "**" (i |-> d))) );
A6: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A7: ( j <> 0 implies F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) ) ; :: thesis: S₁[j + 1]

now :: thesis: S₁[j + 1]

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

suppose A8: j = 0 ; :: thesis: S₁[j + 1]

1 |-> (F "**" (i |-> d)) = <*(F "**" (i |-> d))*> by FINSEQ_2:59;
hence S₁[j + 1] by A8, FINSOP_1:11; :: thesis: verum

end;

suppose A9: j >= 1 + 0 ; :: thesis: S₁[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₁[j + 1] ; :: thesis: verum

end;

end;

end;

hence S₁[j + 1] ; :: thesis: verum

end;

A11: S₁[ 0 ] ;
for j being Nat holds S₁[j] from NAT_1:sch 2(A11, A6);
hence F "**" ((i * j) |-> d) = F "**" (j |-> (F "**" (i |-> d))) by A5; :: thesis: verum

end;

end;