let i be Nat; :: thesis: for S being non empty non void ManySortedSign
for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for T being b₃,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for q being Element of Args (o,T) st i in dom q holds
the_sort_of (q /. i) = (the_arity_of o) /. i
let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for T being b₂,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for q being Element of Args (o,T) st i in dom q holds
the_sort_of (q /. i) = (the_arity_of o) /. i
let o be OperSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for q being Element of Args (o,T) st i in dom q holds
the_sort_of (q /. i) = (the_arity_of o) /. i
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for q being Element of Args (o,T) st i in dom q holds
the_sort_of (q /. i) = (the_arity_of o) /. i
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for q being Element of Args (o,T) st i in dom q holds
the_sort_of (q /. i) = (the_arity_of o) /. i
let q be Element of Args (o,T); :: thesis: ( i in dom q implies the_sort_of (q /. i) = (the_arity_of o) /. i )
assume Z0: i in dom q ; :: thesis: the_sort_of (q /. i) = (the_arity_of o) /. i
then i in dom (the_arity_of o) by MSUALG_3:6;
then ( q /. i = q . i & q . i in the Sorts of T . ((the_arity_of o) /. i) ) by Z0, PARTFUN1:def 6, MSUALG_6:2;
hence the_sort_of (q /. i) = (the_arity_of o) /. i by SORT; :: thesis: verum