let A be free Universal_Algebra; for o1, o2 being Element of Operations A
for p1, p2 being FinSequence st p1 in dom o1 & p2 in dom o2 & o1 . p1 = o2 . p2 holds
( o1 = o2 & p1 = p2 )
let o1, o2 be Element of Operations A; for p1, p2 being FinSequence st p1 in dom o1 & p2 in dom o2 & o1 . p1 = o2 . p2 holds
( o1 = o2 & p1 = p2 )
consider a1 being object such that
A1:
a1 in dom the charact of A
and
A2:
o1 = the charact of A . a1
by FUNCT_1:def 3;
consider a2 being object such that
A3:
a2 in dom the charact of A
and
A4:
o2 = the charact of A . a2
by FUNCT_1:def 3;
reconsider a1 = a1, a2 = a2 as OperSymbol of A by A1, A3;
A5:
o1 = Den (a1,A)
by A2;
A6:
o2 = Den (a2,A)
by A4;
let p1, p2 be FinSequence; ( p1 in dom o1 & p2 in dom o2 & o1 . p1 = o2 . p2 implies ( o1 = o2 & p1 = p2 ) )
assume that
A7:
p1 in dom o1
and
A8:
p2 in dom o2
and
A9:
o1 . p1 = o2 . p2
; ( o1 = o2 & p1 = p2 )
thus
( o1 = o2 & p1 = p2 )
by A5, A6, A7, A8, A9, Th36; verum