let f1, f2 be BinOp of T; :: thesis: ( ( for a, b being Element of T holds f1 . (a,b) = Tern (a,(x `),b) ) & ( for a, b being Element of T holds f2 . (a,b) = Tern (a,(x `),b) ) implies f1 = f2 )
assume that
A1: for a, b being Element of T holds f1 . (a,b) = Tern (a,(x `),b) and
A2: for a, b being Element of T holds f2 . (a,b) = Tern (a,(x `),b) ; :: thesis: f1 = f2
for a, b being Element of T holds f1 . (a,b) = f2 . (a,b)

proof

let a, b be Element of T; :: thesis: f1 . (a,b) = f2 . (a,b)
f1 . (a,b) = Tern (a,(x `),b) by A1
.= f2 . (a,b) by A2 ;
hence f1 . (a,b) = f2 . (a,b) ; :: thesis: verum

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum