let L be non empty multLoopStr_0 ; :: thesis: 1_. L = <%(1. L)%>

A1: dom (0_. L) = NAT by FUNCT_2:def 1;

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

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

let x be object ; :: thesis: ( x in NAT implies (1_. L) . b_{1} = <%(1. L)%> . b_{1} )

assume x in NAT ; :: thesis: (1_. L) . b_{1} = <%(1. L)%> . b_{1}

then reconsider n = x as Element of NAT ;

end;assume x in NAT ; :: thesis: (1_. L) . b

then reconsider n = x as Element of NAT ;