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

now :: thesis: for x being object st x in NAT holds
(1_. L) . x = <%(1. L)%> . x

let x be object ; :: 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:31
.= <%(1. L)%> . x by A2, ALGSEQ_1:def 5 ;
:: thesis: verum

end;

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

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

end;

end;

end;

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