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 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; :: thesis: ( S1[l] implies S1[l + 1] )
assume A2: S1[l] ; :: thesis: S1[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: 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))) ) ; :: thesis: verum