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

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