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:65;

now

let u be set ; :: 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;
dom (0_. L) = NAT by FUNCT_2:def 1;
then 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:66 ;
:: 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:66 ;
:: thesis: verum