let x, y be object ; 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 ; 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; 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; 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; ( 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 )
; AOFA_A00:def 8 ( 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 )
; <*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; verum