let L be non empty unital doubleLoopStr ; :: thesis: for a being Element of L
for i, n being Nat st i <> 0 & i <> n holds
((0_. L) +* ((0,n) --> ((- a),(1. L)))) . i = 0. L
let a be Element of L; :: thesis: for i, n being Nat st i <> 0 & i <> n holds
((0_. L) +* ((0,n) --> ((- a),(1. L)))) . i = 0. L
let i, n be Nat; :: thesis: ( i <> 0 & i <> n implies ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . i = 0. L )
assume that
A1: i <> 0 and
A2: i <> n ; :: thesis: ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . i = 0. L
set t = (0_. L) +* ((0,n) --> ((- a),(1. L)));
set f = (0,n) --> ((- a),(1. L));
A4: for u being object st u in {0,n} holds
u in NAT by ORDINAL1:def 12;
A3: dom ((0,n) --> ((- a),(1. L))) = {0,n} by FUNCT_4:62;
then A5: (dom (0_. L)) \/ (dom ((0,n) --> ((- a),(1. L)))) = NAT by A4, TARSKI:def 3, XBOOLE_1:12;
A6: i in NAT by ORDINAL1:def 12;
not i in dom ((0,n) --> ((- a),(1. L))) by A1, A2, A3, TARSKI:def 2;
hence ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . i = (0_. L) . i by A5, A6, FUNCT_4:def 1
.= 0. L by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum