let L be non empty unital doubleLoopStr ; :: thesis: for n being non zero Nat
for a being Element of L holds
( ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . 0 = - a & ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . n = 1. L )
let n be non zero Nat; :: thesis: for a being Element of L holds
( ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . 0 = - a & ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . n = 1. L )
let a be Element of L; :: thesis: ( ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . 0 = - a & ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . n = 1. L )
set t = (0_. L) +* ((0,n) --> ((- a),(1. L)));
set f = (0,n) --> ((- a),(1. L));
A2: 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 A4: (dom (0_. L)) \/ (dom ((0,n) --> ((- a),(1. L)))) = NAT by A2, TARSKI:def 3, XBOOLE_1:12;
( 0 in dom ((0,n) --> ((- a),(1. L))) & 0 in (dom (0_. L)) \/ (dom ((0,n) --> ((- a),(1. L)))) ) by A4, A3, TARSKI:def 2;
hence ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . 0 = ((0,n) --> ((- a),(1. L))) . 0 by FUNCT_4:def 1
.= - a by FUNCT_4:63 ;
:: thesis: ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . n = 1. L
( n in dom ((0,n) --> ((- a),(1. L))) & n in (dom (0_. L)) \/ (dom ((0,n) --> ((- a),(1. L)))) ) by A4, A3, TARSKI:def 2, ORDINAL1:def 12;
hence ((0_. L) +* ((0,n) --> ((- a),(1. L)))) . n = ((0,n) --> ((- a),(1. L))) . n by FUNCT_4:def 1
.= 1. L by FUNCT_4:63 ;
:: thesis: verum