deffunc H1( object ) -> Element of Q,(() /. \$1) = (In ((p . \$1),( the Sorts of Q . (() /. \$1)))) / (x,y);
consider q being Function such that
A1: ( dom q = dom () & ( for x being object st x in dom () holds
q . x = H1(x) ) ) from dom q = Seg (len ()) by ;
then reconsider q = q as FinSequence by FINSEQ_1:def 2;
A2: len q = len () by ;
now :: thesis: for k being Nat st k in dom q holds
q . k in the Sorts of Q . (() /. k)
let k be Nat; :: thesis: ( k in dom q implies q . k in the Sorts of Q . (() /. k) )
assume A3: k in dom q ; :: thesis: q . k in the Sorts of Q . (() /. k)
q . k = H1(k) by A1, A3;
hence q . k in the Sorts of Q . (() /. k) ; :: thesis: verum
end;
then reconsider q = q as Element of Args (o,Q) by ;
take q ; :: thesis: for i being Nat st i in dom () holds
ex j being SortSymbol of J st
( j = () . 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 () implies ex j being SortSymbol of J st
( j = () . i & ex A being Element of Q,j st
( A = p . i & q . i = A / (x,y) ) ) )

assume A4: i in dom () ; :: thesis: ex j being SortSymbol of J st
( j = () . i & ex A being Element of Q,j st
( A = p . i & q . i = A / (x,y) ) )

take j = () /. i; :: thesis: ( j = () . i & ex A being Element of Q,j st
( A = p . i & q . i = A / (x,y) ) )

thus j = () . i by ; :: 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 ; :: thesis: q . i = A / (x,y)
thus q . i = A / (x,y) by A4, A1; :: thesis: verum