let A be free Universal_Algebra; :: thesis: 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; :: thesis: 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 set such that
A1: ( a1 in dom the charact of A & o1 = the charact of A . a1 ) by FUNCT_1:def 5;
consider a2 being set such that
A2: ( a2 in dom the charact of A & o2 = the charact of A . a2 ) by FUNCT_1:def 5;
reconsider a1 = a1, a2 = a2 as OperSymbol of A by A1, A2;
A3: ( o1 = Den a1,A & o2 = Den a2,A ) by A1, A2;
let p1, p2 be FinSequence; :: thesis: ( p1 in dom o1 & p2 in dom o2 & o1 . p1 = o2 . p2 implies ( o1 = o2 & p1 = p2 ) )
assume ( p1 in dom o1 & p2 in dom o2 & o1 . p1 = o2 . p2 ) ; :: thesis: ( o1 = o2 & p1 = p2 )
hence ( o1 = o2 & p1 = p2 ) by A3, Th36; :: thesis: verum