let L be non empty unital doubleLoopStr ; :: thesis: for n being non trivial Nat holds
( ((0_. L) +* ((1,n) --> ((- (1. L)),(1. L)))) . 1 = - (1. L) & ((0_. L) +* ((1,n) --> ((- (1. L)),(1. L)))) . n = 1. L )
let n be non trivial Nat; :: thesis: ( ((0_. L) +* ((1,n) --> ((- (1. L)),(1. L)))) . 1 = - (1. L) & ((0_. L) +* ((1,n) --> ((- (1. L)),(1. L)))) . n = 1. L )
set t = (0_. L) +* ((1,n) --> ((- (1. L)),(1. L)));
set f = (1,n) --> ((- (1. L)),(1. L));
A5: for u being object st u in {1,n} holds
u in NAT by ORDINAL1:def 12;
A3: dom ((1,n) --> ((- (1. L)),(1. L))) = {1,n} by FUNCT_4:62;
then A4: (dom (0_. L)) \/ (dom ((1,n) --> ((- (1. L)),(1. L)))) = NAT by A5, TARSKI:def 3, XBOOLE_1:12;
A6: n <> 1 by NAT_2:28;
( 1 in dom ((1,n) --> ((- (1. L)),(1. L))) & 1 in (dom (0_. L)) \/ (dom ((1,n) --> ((- (1. L)),(1. L)))) ) by A4, A3, TARSKI:def 2;
hence ((0_. L) +* ((1,n) --> ((- (1. L)),(1. L)))) . 1 = ((1,n) --> ((- (1. L)),(1. L))) . 1 by FUNCT_4:def 1
.= - (1. L) by A6, FUNCT_4:63 ;
:: thesis: ((0_. L) +* ((1,n) --> ((- (1. L)),(1. L)))) . n = 1. L
( n in dom ((1,n) --> ((- (1. L)),(1. L))) & n in (dom (0_. L)) \/ (dom ((1,n) --> ((- (1. L)),(1. L)))) ) by A4, A3, TARSKI:def 2, ORDINAL1:def 12;
hence ((0_. L) +* ((1,n) --> ((- (1. L)),(1. L)))) . n = ((1,n) --> ((- (1. L)),(1. L))) . n by FUNCT_4:def 1
.= 1. L by FUNCT_4:63 ;
:: thesis: verum