let f1, f2 be BinOp of (unionCarrier (S,f,E)); :: thesis: ( ( for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & f1 . (a,b) = x + y ) ) & ( for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & f2 . (a,b) = x + y ) ) implies f1 = f2 )
assume that
A1: for a, b being Element of unionCarrier (S,f,E) ex p1 being Element of S ex x, y being Element of (p1 `1) st
( x = a & y = b & f1 . (a,b) = x + y ) and
A2: for a, b being Element of unionCarrier (S,f,E) ex p2 being Element of S ex x, y being Element of (p2 `1) st
( x = a & y = b & f2 . (a,b) = x + y ) ; :: thesis: f1 = f2

now :: thesis: for a, b being Element of unionCarrier (S,f,E) holds f1 . (a,b) = f2 . (a,b)

let a, b be Element of unionCarrier (S,f,E); :: thesis: f1 . (b₁,b₂) = f2 . (b₁,b₂)
consider p1 being Element of S, x1, y1 being Element of (p1 `1) such that
A3: ( x1 = a & y1 = b & f1 . (a,b) = x1 + y1 ) by A1;
consider p2 being Element of S, x2, y2 being Element of (p2 `1) such that
A4: ( x2 = a & y2 = b & f2 . (a,b) = x2 + y2 ) by A2;

per cases ( p1 <= p2 or p2 <= p1 ) by dasc;

suppose p1 <= p2 ; :: thesis: f1 . (b₁,b₂) = f2 . (b₁,b₂)

then p1 `1 is Subfield of p2 `1 by FIELD_4:7;
then A5: the addF of (p1 `1) = the addF of (p2 `1) || the carrier of (p1 `1) by EC_PF_1:def 1;
[x2,y2] in [: the carrier of (p1 `1), the carrier of (p1 `1):] by A3, A4, ZFMISC_1:def 2;
hence f1 . (a,b) = f2 . (a,b) by A3, A4, A5, FUNCT_1:49; :: thesis: verum

end;

suppose p2 <= p1 ; :: thesis: f1 . (b₁,b₂) = f2 . (b₁,b₂)

then p2 `1 is Subfield of p1 `1 by FIELD_4:7;
then A5: the addF of (p2 `1) = the addF of (p1 `1) || the carrier of (p2 `1) by EC_PF_1:def 1;
[x1,y1] in [: the carrier of (p2 `1), the carrier of (p2 `1):] by A3, A4, ZFMISC_1:def 2;
hence f1 . (a,b) = f2 . (a,b) by A3, A4, A5, FUNCT_1:49; :: thesis: verum

end;

end;

end;

hence f1 = f2 ; :: thesis: verum