let D be non empty set ; for d being Element of D
for g being BinOp of D
for k, l being Nat st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d)))
let d be Element of D; for g being BinOp of D
for k, l being Nat st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d)))
let g be BinOp of D; for k, l being Nat st g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) holds
g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d)))
let k, l be Nat; ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d))) )
defpred S1[ Nat] means for g being BinOp of D
for k being Nat
for d being Element of D st g is associative & ( g is having_a_unity or ( k <> 0 & $1 <> 0 ) ) holds
g "**" ((k * $1) |-> d) = g "**" ($1 |-> (g "**" (k |-> d)));
A1:
for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be
Nat;
( S1[l] implies S1[l + 1] )
assume A2:
S1[
l]
;
S1[l + 1]
let g be
BinOp of
D;
for k being Nat
for d being Element of D st g is associative & ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) holds
g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))let k be
Nat;
for d being Element of D st g is associative & ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) holds
g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))let d be
Element of
D;
( g is associative & ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) implies g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) )
assume that A3:
g is
associative
and A4:
(
g is
having_a_unity or (
k <> 0 &
l + 1
<> 0 ) )
;
g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))
now g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))per cases
( l = 0 or l <> 0 )
;
suppose A5:
l <> 0
;
g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))then A6:
(
k <> 0 implies
k * l <> 0 )
by XCMPLX_1:6;
g "**" ((k * (l + 1)) |-> d) =
g "**" (((k * l) + (k * 1)) |-> d)
.=
g . (
(g "**" ((k * l) |-> d)),
(g "**" (k |-> d)))
by A3, A4, A6, Th18
.=
g . (
(g "**" (l |-> (g "**" (k |-> d)))),
(g "**" (k |-> d)))
by A2, A3, A4, A5
.=
g . (
(g "**" (l |-> (g "**" (k |-> d)))),
(g "**" (1 |-> (g "**" (k |-> d)))))
by Th16
;
hence
g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))
by A3, A5, Th18;
verum end; end; end;
hence
g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))
;
verum
end;
A7:
S1[ 0 ]
;
for l being Nat holds S1[l]
from NAT_1:sch 2(A7, A1);
hence
( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d))) )
; verum