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 6
.= ((M # ) * the Arity of S) . o1 by FUNCT_2:21
.= Args o1,A by MSUALG_1:def 9 ;
A2: (M # ) . (the_arity_of o2) = (M # ) . (the Arity of S . o2) by MSUALG_1:def 6
.= ((M # ) * the Arity of S) . o2 by FUNCT_2:21
.= Args o2,A by MSUALG_1:def 9 ;
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