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