let L be non empty unital doubleLoopStr ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( ((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;

now :: thesis: for u being object st u in {0,k} holds
u in NAT

let u be object ; :: thesis: ( u in {0,k} implies u in NAT )
assume u in {0,k} ; :: thesis: u in NAT
then ( u = 0 or u = k ) by TARSKI:def 2;
hence u in NAT ; :: thesis: verum

end;

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