let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty disjoint_valued MSAlgebra over S
for B being non-empty MSAlgebra over S
for f1, f2 being ManySortedFunction of A,B st ( for a being Element of A holds f1 . a = f2 . a ) holds
f1 = f2
let A be non-empty disjoint_valued MSAlgebra over S; :: thesis: for B being non-empty MSAlgebra over S
for f1, f2 being ManySortedFunction of A,B st ( for a being Element of A holds f1 . a = f2 . a ) holds
f1 = f2
let B be non-empty MSAlgebra over S; :: thesis: for f1, f2 being ManySortedFunction of A,B st ( for a being Element of A holds f1 . a = f2 . a ) holds
f1 = f2
let f1, f2 be ManySortedFunction of A,B; :: thesis: ( ( for a being Element of A holds f1 . a = f2 . a ) implies f1 = f2 )
assume Z0: for a being Element of A holds f1 . a = f2 . a ; :: thesis: f1 = f2
let s be SortSymbol of S; :: according to PBOOLE:def 21 :: thesis: f1 . s = f2 . s
now :: thesis: ( f1 . s is Function of ( the Sorts of A . s),( the Sorts of B . s) & f2 . s is Function of ( the Sorts of A . s),( the Sorts of B . s) & ( for a being Element of the Sorts of A . s holds (f1 . s) . a = (f2 . s) . a ) )
thus ( f1 . s is Function of ( the Sorts of A . s),( the Sorts of B . s) & f2 . s is Function of ( the Sorts of A . s),( the Sorts of B . s) ) ; :: thesis: for a being Element of the Sorts of A . s holds (f1 . s) . a = (f2 . s) . a
let a be Element of the Sorts of A . s; :: thesis: (f1 . s) . a = (f2 . s) . a
thus (f1 . s) . a = f1 . a by Th9
.= f2 . a by Z0
.= (f2 . s) . a by Th9 ; :: thesis: verum
end;
hence f1 . s = f2 . s by FUNCT_2:def 8; :: thesis: verum