deffunc H1( 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 = H1(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;
then reconsider q = q as Element of Args (o,Q) by A2, MSAFREE2:5;
take
q
; 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; ( 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)
; 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; ( 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; 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)); ( A = p . i & q . i = A / (x,y) )
thus
A = p . i
by A4, MSUALG_6:2, SUBSET_1:def 8; q . i = A / (x,y)
thus
q . i = A / (x,y)
by A4, A1; verum