deffunc H1( Element of Fin I) -> Element of L = Sum (x,$1);
A2:
for a, b being Function of (Fin I), the carrier of L st ( for q being Element of Fin I holds a . q = H1(q) ) & ( for q being Element of Fin I holds b . q = H1(q) ) holds
a = b
from BINOP_2:sch 1();
let f, g be Function of ([#] (OrderedFIN I)), the carrier of L; ( ( for j being Element of Fin I holds f . j = Sum (x,j) ) & ( for j being Element of Fin I holds g . j = Sum (x,j) ) implies f = g )
assume that
A3:
for j being Element of Fin I holds f . j = Sum (x,j)
and
A4:
for j being Element of Fin I holds g . j = Sum (x,j)
; f = g
the carrier of (OrderedFIN I) = Fin I
by YELLOW_1:1;
then
[#] (OrderedFIN I) = Fin I
by STRUCT_0:def 3;
then reconsider f = f, g = g as Function of (Fin I), the carrier of L ;
f = g
by A2, A3, A4;
hence
f = g
; verum