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 ;
( n in dom ((0,n) --> ((1. L),(1. L))) & n in (dom (0_. L)) \/ (dom ((0,n) --> ((1. L),(1. L)))) ) by ;
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 ;
hence ((0_. L) +* ((0,n) --> ((1. L),(1. L)))) . 0 = ((0,n) --> ((1. L),(1. L))) . 0 by
.= 1. L by ;
:: 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;