let R be non empty unital right_zeroed doubleLoopStr ; for a, b being Element of R holds (a,b) In_Power 0 = <*(1_ R)*>
let a, b be Element of R; (a,b) In_Power 0 = <*(1_ R)*>
set p = (a,b) In_Power 0;
A1: len ((a,b) In_Power 0) =
0 + 1
by Def7
.=
1
;
then A2:
dom ((a,b) In_Power 0) = {1}
by FINSEQ_1:2, FINSEQ_1:def 3;
then A3:
1 in dom ((a,b) In_Power 0)
by TARSKI:def 1;
then consider i being Element of NAT such that
A4:
i in dom ((a,b) In_Power 0)
;
A5:
i = 1
by A2, A4, TARSKI:def 1;
then reconsider m = i - 1 as Element of NAT by INT_1:5;
reconsider l = 0 - m as Element of NAT by A5;
((a,b) In_Power 0) . 1 =
((a,b) In_Power 0) /. 1
by A3, PARTFUN1:def 6
.=
((0 choose m) * (a |^ l)) * (b |^ m)
by A3, A5, Def7
.=
(1 * (a |^ l)) * (b |^ m)
by A5, NEWTON:19
.=
(1 * (a |^ 0)) * (1_ R)
by A5, Th8
.=
(1 * (1_ R)) * (1_ R)
by Th8
.=
(1_ R) * (1_ R)
by Th13
.=
1_ R
by GROUP_1:def 4
;
hence
(a,b) In_Power 0 = <*(1_ R)*>
by A1, FINSEQ_1:40; verum