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