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)

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

hence
f1 = f2
by BINOP_1:2; :: thesis: verum
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;f1 . (a,b) = Tern (a,(x `),b) by A1

.= f2 . (a,b) by A2 ;

hence f1 . (a,b) = f2 . (a,b) ; :: thesis: verum