let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( g is associative & ( g is having_a_unity or ( k <> 0 & l <> 0 ) ) implies g "**" ((k * l) |-> d) = g "**" (l |-> (g "**" (k |-> d))) )
defpred S₁[ 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 S₁[l] holds
S₁[l + 1]

proof

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A2: S₁[l] ; :: thesis: S₁[l + 1]
let g be BinOp of D; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ) ; :: thesis: g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))

now :: thesis: g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))

per cases ( l = 0 or l <> 0 ) ;

suppose l = 0 ; :: thesis: g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))

hence g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) by Th16; :: thesis: verum

end;

suppose A5: l <> 0 ; :: thesis: 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; :: thesis: verum

end;

end;

end;

hence g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) ; :: thesis: verum

end;

A7: S₁[ 0 ] ;
for l being Nat holds S₁[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))) ) ; :: thesis: verum