let S be OrderSortedSign; :: thesis: for o1, o2 being OperSymbol of S
for A being OSAlgebra of S st the_arity_of o1 <= the_arity_of o2 holds
Args (o1,A) c= Args (o2,A)
let o1, o2 be OperSymbol of S; :: thesis: for A being OSAlgebra of S st the_arity_of o1 <= the_arity_of o2 holds
Args (o1,A) c= Args (o2,A)
let A be OSAlgebra of S; :: thesis: ( the_arity_of o1 <= the_arity_of o2 implies Args (o1,A) c= Args (o2,A) )
reconsider M = the Sorts of A as OrderSortedSet of S by Th17;
A1: (M #) . (the_arity_of o1) = (M #) . ( the Arity of S . o1) by MSUALG_1:def 1
.= ((M #) * the Arity of S) . o1 by FUNCT_2:15
.= Args (o1,A) by MSUALG_1:def 4 ;
A2: (M #) . (the_arity_of o2) = (M #) . ( the Arity of S . o2) by MSUALG_1:def 1
.= ((M #) * the Arity of S) . o2 by FUNCT_2:15
.= Args (o2,A) by MSUALG_1:def 4 ;
assume the_arity_of o1 <= the_arity_of o2 ; :: thesis: Args (o1,A) c= Args (o2,A)
hence Args (o1,A) c= Args (o2,A) by A1, A2, Th20; :: thesis: verum