let x, y be object ; :: thesis: for S being non empty non void ManySortedSign

for o being OperSymbol of S

for s1, s2, r being SortSymbol of S

for T being MSAlgebra over S st o is_of_type <*s1,s2*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 holds

<*x,y*> in Args (o,T)

let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S

for s1, s2, r being SortSymbol of S

for T being MSAlgebra over S st o is_of_type <*s1,s2*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 holds

<*x,y*> in Args (o,T)

let o be OperSymbol of S; :: thesis: for s1, s2, r being SortSymbol of S

for T being MSAlgebra over S st o is_of_type <*s1,s2*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 holds

<*x,y*> in Args (o,T)

let s1, s2, r be SortSymbol of S; :: thesis: for T being MSAlgebra over S st o is_of_type <*s1,s2*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 holds

<*x,y*> in Args (o,T)

let A be MSAlgebra over S; :: thesis: ( o is_of_type <*s1,s2*>,r & x in the Sorts of A . s1 & y in the Sorts of A . s2 implies <*x,y*> in Args (o,A) )

assume A1: ( the Arity of S . o = <*s1,s2*> & 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 <*x,y*> in Args (o,A) )

assume A2: ( x in the Sorts of A . s1 & y in the Sorts of A . s2 ) ; :: thesis: <*x,y*> in Args (o,A)

then reconsider x = x as Element of the Sorts of A . s1 ;

reconsider y = y as Element of the Sorts of A . s2 by A2;

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)*> by A1, A3, FINSEQ_2:36 ;

hence <*x,y*> in Args (o,A) by A2, FINSEQ_3:124; :: thesis: verum

for o being OperSymbol of S

for s1, s2, r being SortSymbol of S

for T being MSAlgebra over S st o is_of_type <*s1,s2*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 holds

<*x,y*> in Args (o,T)

let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S

for s1, s2, r being SortSymbol of S

for T being MSAlgebra over S st o is_of_type <*s1,s2*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 holds

<*x,y*> in Args (o,T)

let o be OperSymbol of S; :: thesis: for s1, s2, r being SortSymbol of S

for T being MSAlgebra over S st o is_of_type <*s1,s2*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 holds

<*x,y*> in Args (o,T)

let s1, s2, r be SortSymbol of S; :: thesis: for T being MSAlgebra over S st o is_of_type <*s1,s2*>,r & x in the Sorts of T . s1 & y in the Sorts of T . s2 holds

<*x,y*> in Args (o,T)

let A be MSAlgebra over S; :: thesis: ( o is_of_type <*s1,s2*>,r & x in the Sorts of A . s1 & y in the Sorts of A . s2 implies <*x,y*> in Args (o,A) )

assume A1: ( the Arity of S . o = <*s1,s2*> & 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 <*x,y*> in Args (o,A) )

assume A2: ( x in the Sorts of A . s1 & y in the Sorts of A . s2 ) ; :: thesis: <*x,y*> in Args (o,A)

then reconsider x = x as Element of the Sorts of A . s1 ;

reconsider y = y as Element of the Sorts of A . s2 by A2;

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)*> by A1, A3, FINSEQ_2:36 ;

hence <*x,y*> in Args (o,A) by A2, FINSEQ_3:124; :: thesis: verum