let n be Nat; :: thesis: for L being non empty unital doubleLoopStr holds
( ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . 0 = 1. L & ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . n = 1. L )
let L be non empty unital doubleLoopStr ; :: thesis: ( ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . 0 = 1. L & ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . n = 1. 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;
A7: 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;
( n in dom ((0,n) --> ((1. L),(1. L))) & n in (dom (0_. L)) \/ (dom ((0,n) --> ((1. L),(1. L)))) ) by A5, A7, TARSKI:def 2, ORDINAL1:def 12;
then A10: ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . n = ((0,n) --> ((1. L),(1. L))) . n by FUNCT_4:def 1
.= 1. L by FUNCT_4:63 ;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: ( ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . 0 = 1. L & ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . n = 1. L )

hence ( ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . 0 = 1. L & ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . n = 1. L ) by A10; :: thesis: verum

end;

suppose A6: n <> 0 ; :: thesis: ( ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . 0 = 1. L & ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . n = 1. L )

0 in dom ((0,n) --> ((1. L),(1. L))) by A7, TARSKI:def 2;
hence ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . 0 = ((0,n) --> ((1. L),(1. L))) . 0 by A5, FUNCT_4:def 1
.= 1. L by A6, FUNCT_4:63 ;
:: thesis: ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . n = 1. L
thus ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . n = 1. L by A10; :: thesis: verum

end;

end;