deffunc H_{1}( Element of Fin I) -> Element of L = Sum (x,$1);

A3: for a, b being Function of (Fin I), the carrier of L st ( for q being Element of Fin I holds a . q = H_{1}(q) ) & ( for q being Element of Fin I holds b . q = H_{1}(q) ) holds

a = b from BINOP_2:sch 1();

let f, g be Function of ([#] (OrderedFIN I)), the carrier of L; :: thesis: ( ( 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

A4: for j being Element of Fin I holds f . j = Sum (x,j) and

A5: for j being Element of Fin I holds g . j = Sum (x,j) ; :: thesis: 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 A3, A4, A5;

hence f = g ; :: thesis: verum

A3: for a, b being Function of (Fin I), the carrier of L st ( for q being Element of Fin I holds a . q = H

a = b from BINOP_2:sch 1();

let f, g be Function of ([#] (OrderedFIN I)), the carrier of L; :: thesis: ( ( 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

A4: for j being Element of Fin I holds f . j = Sum (x,j) and

A5: for j being Element of Fin I holds g . j = Sum (x,j) ; :: thesis: 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 A3, A4, A5;

hence f = g ; :: thesis: verum