let L be non empty unital doubleLoopStr ; :: thesis: for z being Element of L
for k being Element of NAT
for i being Nat st i <> 0 & i <> k holds
((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L
let z be Element of L; :: thesis: for k being Element of NAT
for i being Nat st i <> 0 & i <> k holds
((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L
let k be Element of NAT ; :: thesis: for i being Nat st i <> 0 & i <> k holds
((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L
let i be Nat; :: thesis: ( i <> 0 & i <> k implies ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L )
assume that
A1: i <> 0 and
A2: i <> k ; :: thesis: ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L
set t = (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)));
set f = (0,k) --> ((- ((power L) . (z,k))),(1_ L));

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 A4: {0,k} c= NAT by TARSKI:def 3;
dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) = {0,k} by FUNCT_4:62;
then A5: (dom (0_. L)) \/ (dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) = NAT by A4, XBOOLE_1:12;
A6: i in NAT by ORDINAL1:def 12;
not i in dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) by A1, A2, TARSKI:def 2;
hence ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = (0_. L) . i by A5, A6, FUNCT_4:def 1
.= 0. L by A6, FUNCOP_1:7 ;
:: thesis: verum