let x, y, z be object ; :: thesis: for S being non empty non void ManySortedSign
for o being OperSymbol of S
for s1, s2, s3, r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type <*s1,s2,s3*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 & z in the Sorts of T . s3 holds
<*x,y,z*> in Args (o,T)
let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for s1, s2, s3, r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type <*s1,s2,s3*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 & z in the Sorts of T . s3 holds
<*x,y,z*> in Args (o,T)
let o be OperSymbol of S; :: thesis: for s1, s2, s3, r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type <*s1,s2,s3*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 & z in the Sorts of T . s3 holds
<*x,y,z*> in Args (o,T)
let s1, s2, s3, r be SortSymbol of S; :: thesis: for T being MSAlgebra over S st o is_of_type <*s1,s2,s3*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 & z in the Sorts of T . s3 holds
<*x,y,z*> in Args (o,T)
let A be MSAlgebra over S; :: thesis: ( o is_of_type <*s1,s2,s3*>,r & x in the Sorts of A . s1 & y in the Sorts of A . s2 & z in the Sorts of A . s3 implies <*x,y,z*> in Args (o,A) )
assume A1: ( the Arity of S . o = <*s1,s2,s3*> & the ResultSort of S . o = r ) ; :: according to AOFA_A00:def 8 :: thesis: ( not x in the Sorts of A . s1 or not y in the Sorts of A . s2 or not z in the Sorts of A . s3 or <*x,y,z*> in Args (o,A) )
assume A2: ( x in the Sorts of A . s1 & y in the Sorts of A . s2 & z in the Sorts of A . s3 ) ; :: thesis: <*x,y,z*> in Args (o,A)
A3: the Sorts of A is Function of the carrier of S,(bool (Union the Sorts of A)) by Lm1;
Args (o,A) = product ( the Sorts of A * (the_arity_of o)) by PRALG_2:3
.= product <*( the Sorts of A . s1),( the Sorts of A . s2),( the Sorts of A . s3)*> by A1, A3, FINSEQ_2:37 ;
hence <*x,y,z*> in Args (o,A) by A2, FINSEQ_3:125; :: thesis: verum