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 5
.= the Sorts of A . ( the ResultSort of S . o2) by FUNCT_2:15
.= the Sorts of A . (the_result_sort_of o2) by MSUALG_1:def 2 ;
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 Def16;
Result (o1,A) = ( the Sorts of A * the ResultSort of S) . o1 by MSUALG_1:def 5
.= the Sorts of A . ( the ResultSort of S . o1) by FUNCT_2:15
.= the Sorts of A . (the_result_sort_of o1) by MSUALG_1:def 2 ;
hence Result (o1,A) c= Result (o2,A) by A2, A1; :: thesis: verum