let S be OrderSortedSign; :: thesis: for o1, o2 being OperSymbol of S
for A being OSAlgebra of S st the_result_sort_of o1 <= the_result_sort_of o2 holds
Result o1,A c= Result o2,A
let o1, o2 be OperSymbol of S; :: thesis: for A being OSAlgebra of S st the_result_sort_of o1 <= the_result_sort_of o2 holds
Result o1,A c= Result o2,A
let A be OSAlgebra of S; :: thesis: ( the_result_sort_of o1 <= the_result_sort_of o2 implies Result o1,A c= Result o2,A )
reconsider M = the Sorts of A as OrderSortedSet of S by Th17;
A1: Result o2,A = (the Sorts of A * the ResultSort of S) . o2 by MSUALG_1:def 10
.= the Sorts of A . (the ResultSort of S . o2) by FUNCT_2:21
.= the Sorts of A . (the_result_sort_of o2) by MSUALG_1:def 7 ;
assume the_result_sort_of o1 <= the_result_sort_of o2 ; :: thesis: Result o1,A c= Result o2,A
then A2: M . (the_result_sort_of o1) c= M . (the_result_sort_of o2) by Def18;
Result o1,A = (the Sorts of A * the ResultSort of S) . o1 by MSUALG_1:def 10
.= the Sorts of A . (the ResultSort of S . o1) by FUNCT_2:21
.= the Sorts of A . (the_result_sort_of o1) by MSUALG_1:def 7 ;
hence Result o1,A c= Result o2,A by A2, A1; :: thesis: verum