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);
A3: dom (0_. L) = NAT by FUNCT_2:def 1;

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 A4: {0 ,k} c= NAT by TARSKI:def 3;
dom (0 ,k --> (- ((power L) . z,k)),(1_ L)) = {0 ,k} by FUNCT_4:65;
then A5: (dom (0_. L)) \/ (dom (0 ,k --> (- ((power L) . z,k)),(1_ L))) = NAT by A3, A4, XBOOLE_1:12;
A6: i in NAT by ORDINAL1:def 13;
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:13 ;
:: thesis: verum