let f1, f2 be BinOp of Q; :: thesis: ( ( for p, q being FinSequence st p in Q & q in Q holds
f1 . (p,q) = t ^ (p ^ q) ) & ( for p, q being FinSequence st p in Q & q in Q holds
f2 . (p,q) = t ^ (p ^ q) ) implies f1 = f2 )
assume that
A1: for p, q being FinSequence st p in Q & q in Q holds
f1 . (p,q) = t ^ (p ^ q) and
A2: for p, q being FinSequence st p in Q & q in Q holds
f2 . (p,q) = t ^ (p ^ q) ; :: thesis: f1 = f2
for p, q being Element of Q holds f1 . (p,q) = f2 . (p,q)

proof

let p, q be Element of Q; :: thesis: f1 . (p,q) = f2 . (p,q)
thus f1 . (p,q) = t ^ (p ^ q) by A1
.= f2 . (p,q) by A2 ; :: thesis: verum

end;

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