let L be non empty multLoopStr_0 ; :: thesis: 1_. L = <%(1. L)%>
A1: dom (0_. L) = NAT by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in NAT implies (1_. L) . b₁ = <%(1. L)%> . b₁ )
assume x in NAT ; :: thesis: (1_. L) . b₁ = <%(1. L)%> . b₁
then reconsider n = x as Element of NAT ;

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

suppose A2: x = 0 ; :: thesis: (1_. L) . b₁ = <%(1. L)%> . b₁

hence (1_. L) . x = 1. L by A1, FUNCT_7:33
.= <%(1. L)%> . x by A2, ALGSEQ_1:def 6 ;
:: thesis: verum

end;

suppose A3: n <> 0 ; :: thesis: (1_. L) . b₁ = <%(1. L)%> . b₁

then A4: ( n = 1 or n > 1 ) by NAT_1:54;
thus (1_. L) . x = (0_. L) . n by A3, FUNCT_7:34
.= 0. L by FUNCOP_1:13
.= <%(1. L)%> . x by A4, POLYNOM5:33 ; :: thesis: verum

end;

end;

end;

hence 1_. L = <%(1. L)%> by FUNCT_2:18; :: thesis: verum