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