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