deffunc H_{1}( 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_{1}(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;

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

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

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)

then reconsider q = q as Element of Args (o,Q) by A2, MSAFREE2:5;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_{1}(k)
by A1, A3;

hence q . k in the Sorts of Q . ((the_arity_of o) /. k) ; :: thesis: verum

end;assume A3: k in dom q ; :: thesis: q . k in the Sorts of Q . ((the_arity_of o) /. k)

q . k = H

hence q . k in the Sorts of Q . ((the_arity_of o) /. k) ; :: thesis: verum

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