let f1, f2 be BinOp of Z; ( ( for q, r being FinSequence st q in Z & r in Z holds
f1 . (q,r) = p ^ (q ^ r) ) & ( for q, r being FinSequence st q in Z & r in Z holds
f2 . (q,r) = p ^ (q ^ r) ) implies f1 = f2 )
assume that
A1:
for q, r being FinSequence st q in Z & r in Z holds
f1 . (q,r) = p ^ (q ^ r)
and
A2:
for q, r being FinSequence st q in Z & r in Z holds
f2 . (q,r) = p ^ (q ^ r)
; f1 = f2
for q, r being Element of Z holds f1 . (q,r) = f2 . (q,r)
proof
let q,
r be
Element of
Z;
f1 . (q,r) = f2 . (q,r)
thus f1 . (
q,
r) =
p ^ (q ^ r)
by A1
.=
f2 . (
q,
r)
by A2
;
verum
end;
hence
f1 = f2
by BINOP_1:2; verum