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) . b1 = <%(1. L)%> . b1 )
assume x in NAT ; :: thesis: (1_. L) . b1 = <%(1. L)%> . b1
then reconsider n = x as Element of NAT ;
per cases ( x = 0 or n <> 0 ) ;
suppose A2: x = 0 ; :: thesis: (1_. L) . b1 = <%(1. L)%> . b1
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) . b1 = <%(1. L)%> . b1
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