let D be non empty set ; :: thesis: for d being Element of D
for g being BinOp of D
for k, l being Element of 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 Element of 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 Element of 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 Element of 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₁[ Element of NAT ] means for g being BinOp of D
for k being Element of 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: S₁[ 0 ]

proof

let g be BinOp of D; :: thesis: for k being Element of NAT
for d being Element of D st g is associative & ( g is having_a_unity or ( k <> 0 & 0 <> 0 ) ) holds
g "**" ((k * 0 ) |-> d) = g "**" (0 |-> (g "**" (k |-> d)))
let k be Element of NAT ; :: thesis: for d being Element of D st g is associative & ( g is having_a_unity or ( k <> 0 & 0 <> 0 ) ) holds
g "**" ((k * 0 ) |-> d) = g "**" (0 |-> (g "**" (k |-> d)))
let d be Element of D; :: thesis: ( g is associative & ( g is having_a_unity or ( k <> 0 & 0 <> 0 ) ) implies g "**" ((k * 0 ) |-> d) = g "**" (0 |-> (g "**" (k |-> d))) )
assume ( g is associative & ( g is having_a_unity or ( k <> 0 & 0 <> 0 ) ) ) ; :: thesis: g "**" ((k * 0 ) |-> d) = g "**" (0 |-> (g "**" (k |-> d)))
thus g "**" ((k * 0 ) |-> d) = g "**" (<*> D) by FINSEQ_2:72
.= g "**" (0 |-> (g "**" (k |-> d))) by FINSEQ_2:72 ; :: thesis: verum

end;

A2: for l being Element of NAT st S₁[l] holds
S₁[l + 1]

proof

let l be Element of NAT ; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A3: S₁[l] ; :: thesis: S₁[l + 1]
let g be BinOp of D; :: thesis: for k being Element of 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 Element of 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
A4: g is associative and
A5: ( g is having_a_unity or ( k <> 0 & l + 1 <> 0 ) ) ; :: thesis: g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d)))

now

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 Th17; :: thesis: verum

end;

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

then A7: ( 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 A4, A5, A7, Th19
.= g . (g "**" (l |-> (g "**" (k |-> d)))),(g "**" (k |-> d)) by A3, A4, A5, A6
.= g . (g "**" (l |-> (g "**" (k |-> d)))),(g "**" (1 |-> (g "**" (k |-> d)))) by Th17 ;
hence g "**" ((k * (l + 1)) |-> d) = g "**" ((l + 1) |-> (g "**" (k |-> d))) by A4, A6, Th19; :: thesis: verum

end;

end;

end;

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

end;

for l being Element of NAT holds S₁[l] from NAT_1:sch 1(A1, A2);
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