deffunc H₁( object ) -> Element of Q,((the_arity_of o) /. $1) = (In ((p . $1),( the Sorts of Q . ((the_arity_of o) /. $1)))) / (x,y);
consider q being Function such that
A1: ( dom q = dom (the_arity_of o) & ( for x being object st x in dom (the_arity_of o) holds
q . x = H₁(x) ) ) from FUNCT_1:sch 3();
dom q = Seg (len (the_arity_of o)) by A1, FINSEQ_1:def 3;
then reconsider q = q as FinSequence by FINSEQ_1:def 2;
A2: len q = len (the_arity_of o) by A1, FINSEQ_3:29;

now :: thesis: for k being Nat st k in dom q holds
q . k in the Sorts of Q . ((the_arity_of o) /. k)

let k be Nat; :: thesis: ( k in dom q implies q . k in the Sorts of Q . ((the_arity_of o) /. k) )
assume A3: k in dom q ; :: thesis: q . k in the Sorts of Q . ((the_arity_of o) /. k)
q . k = H₁(k) by A1, A3;
hence q . k in the Sorts of Q . ((the_arity_of o) /. k) ; :: thesis: verum

end;

then reconsider q = q as Element of Args (o,Q) by A2, MSAFREE2:5;
take q ; :: thesis: for i being Nat st i in dom (the_arity_of o) holds
ex j being SortSymbol of J st
( j = (the_arity_of o) . i & ex A being Element of Q,j st
( A = p . i & q . i = A / (x,y) ) )
let i be Nat; :: thesis: ( i in dom (the_arity_of o) implies ex j being SortSymbol of J st
( j = (the_arity_of o) . i & ex A being Element of Q,j st
( A = p . i & q . i = A / (x,y) ) ) )
assume A4: i in dom (the_arity_of o) ; :: thesis: ex j being SortSymbol of J st
( j = (the_arity_of o) . i & ex A being Element of Q,j st
( A = p . i & q . i = A / (x,y) ) )
take j = (the_arity_of o) /. i; :: thesis: ( j = (the_arity_of o) . i & ex A being Element of Q,j st
( A = p . i & q . i = A / (x,y) ) )
thus j = (the_arity_of o) . i by A4, PARTFUN1:def 6; :: thesis: ex A being Element of Q,j st
( A = p . i & q . i = A / (x,y) )
take A = In ((p . i),( the Sorts of Q . j)); :: thesis: ( A = p . i & q . i = A / (x,y) )
thus A = p . i by A4, MSUALG_6:2, SUBSET_1:def 8; :: thesis: q . i = A / (x,y)
thus q . i = A / (x,y) by A4, A1; :: thesis: verum