s9 in rng (the_arity_of o9) by DEP;
then consider i being object such that
A1: ( i in dom (the_arity_of o9) & s9 = (the_arity_of o9) . i ) by FUNCT_1:def 3;
reconsider i = i as Nat by A1;
A2: s9 = (the_arity_of o9) /. i by A1, PARTFUN1:def 6;
deffunc H1( Nat) -> Element of Union the Sorts of (Free (S9,X9)) = IFEQ (S9,i,(x9 -term),( the x9 -different Element of X9 . ((the_arity_of o9) /. S9) -term));
consider f being FinSequence such that
A3: ( len f = len (the_arity_of o9) & ( for i being Nat st i in dom f holds
f . i = H1(i) ) ) from FINSEQ_1:sch 2();
now :: thesis: for j being Nat st j in dom f holds
f . j in the Sorts of (Free (S9,X9)) . ((the_arity_of o9) /. j)
let j be Nat; :: thesis: ( j in dom f implies f . j in the Sorts of (Free (S9,X9)) . ((the_arity_of o9) /. j) )
assume j in dom f ; :: thesis: f . j in the Sorts of (Free (S9,X9)) . ((the_arity_of o9) /. j)
then ( f . j = H1(j) & ( i = j or i <> j ) ) by A3;
then ( ( i = j & f . j = x9 -term ) or f . j = the x9 -different Element of X9 . ((the_arity_of o9) /. j) -term ) by FUNCOP_1:def 8;
hence f . j in the Sorts of (Free (S9,X9)) . ((the_arity_of o9) /. j) by A2; :: thesis: verum
end;
then reconsider f = f as Element of Args (o9,(Free (S9,X9))) by A3, MSAFREE2:5;
take f ; :: thesis: f is x9 -context_including
take i ; :: according to MSAFREE5:def 24 :: thesis: ( i in dom f & f . i is context of x9 & ( for j being Nat
for t being Element of (Free (S9,X9)) st j in dom f & j <> i & t = f . j holds
t is x9 -omitting ) )
thus i in dom f by A1, A3, FINSEQ_3:29; :: thesis: ( f . i is context of x9 & ( for j being Nat
for t being Element of (Free (S9,X9)) st j in dom f & j <> i & t = f . j holds
t is x9 -omitting ) )
then f . i = H1(i) by A3
.= x9 -term by FUNCOP_1:def 8 ;
hence f . i is context of x9 ; :: thesis: for j being Nat
for t being Element of (Free (S9,X9)) st j in dom f & j <> i & t = f . j holds
t is x9 -omitting
let j be Nat; :: thesis: for t being Element of (Free (S9,X9)) st j in dom f & j <> i & t = f . j holds
t is x9 -omitting
let t be Element of (Free (S9,X9)); :: thesis: ( j in dom f & j <> i & t = f . j implies t is x9 -omitting )
assume ( j in dom f & j <> i ) ; :: thesis: ( not t = f . j or t is x9 -omitting )
then ( f . j = H1(j) & H1(j) = the x9 -different Element of X9 . ((the_arity_of o9) /. j) -term ) by A3, FUNCOP_1:def 8;
hence ( t = f . j implies t is x9 -omitting ) ; :: thesis: verum