let L be non empty unital doubleLoopStr ; for z being Element of L
for k being Element of NAT st k <> 0 holds
( ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . 0 = - ((power L) . (z,k)) & ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . k = 1_ L )
let z be Element of L; for k being Element of NAT st k <> 0 holds
( ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . 0 = - ((power L) . (z,k)) & ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . k = 1_ L )
let k be Element of NAT ; ( k <> 0 implies ( ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . 0 = - ((power L) . (z,k)) & ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . k = 1_ L ) )
assume A1:
k <> 0
; ( ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . 0 = - ((power L) . (z,k)) & ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . k = 1_ L )
set t = (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)));
set f = (0,k) --> ((- ((power L) . (z,k))),(1_ L));
set a = - ((power L) . (z,k));
A2:
dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) = {0,k}
by FUNCT_4:62;
then A3:
{0,k} c= NAT
by TARSKI:def 3;
A4:
(dom (0_. L)) \/ (dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) = NAT
by A2, A3, XBOOLE_1:12;
0 in dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))
by A2, TARSKI:def 2;
hence ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . 0 =
((0,k) --> ((- ((power L) . (z,k))),(1_ L))) . 0
by A4, FUNCT_4:def 1
.=
- ((power L) . (z,k))
by A1, FUNCT_4:63
;
((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . k = 1_ L
k in dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))
by A2, TARSKI:def 2;
hence ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . k =
((0,k) --> ((- ((power L) . (z,k))),(1_ L))) . k
by A4, FUNCT_4:def 1
.=
1_ L
by FUNCT_4:63
;
verum