let m be Element of NAT ; :: thesis:
let S be non empty non void ManySortedSign ; :: thesis:
let s be SortSymbol of S; :: thesis:
let o be OperSymbol of S; :: thesis:
let Y be infinite-yielding ManySortedSet of the carrier of S; :: thesis:
let q be Element of Args (o,(Free (S,Y))); :: thesis:
let V be finite set ; :: thesis:
assume Z0: ( m in dom q & (the_arity_of o) /. m = s ) ; :: thesis:
set y = the Element of (Y . s) \ (V \/ (proj1 (rng (o -term q))));
A0: proj1 (rng (o -term q)) is finite by WAYBEL26:39;
then reconsider y = the Element of (Y . s) \ (V \/ (proj1 (rng (o -term q)))) as Element of Y . s by XBOOLE_0:def 5;
reconsider t = y -term as Element of (Free (S,Y)) ;
reconsider q1 = q +* (m,(y -term)) as Element of Args (o,(Free (S,Y))) by Z0, MSUALG_6:7;
A1: q1 is y -context_including

proof

take m ; :: according to MSAFREE5:def 24 :: thesis:
thus m in dom q1 by Z0, FUNCT_7:30; :: thesis:
thus q1 . m is context of y by Z0, FUNCT_7:31; :: thesis:
let j be Nat; :: thesis:
let v be Element of (Free (S,Y)); :: thesis:
assume Z1: ( j in dom q1 & j <> m & v = q1 . j ) ; :: thesis:
then A4: j in dom q by FUNCT_7:30;
then A2: ( v = q . j & q . j in rng q ) by Z1, FUNCT_7:32, FUNCT_1:def 3;
set d = the Element of Coim (v,[y,s]);
assume A7: Coim (v,[y,s]) <> {} ; :: according to MSAFREE5:def 21 :: thesis:
then A3: ( the Element of Coim (v,[y,s]) in dom v & v . the Element of Coim (v,[y,s]) in {[y,s]} ) by FUNCT_1:def 7;
reconsider d = the Element of Coim (v,[y,s]) as Element of dom v by A7, FUNCT_1:def 7;
consider k being Nat such that
A5: j = 1 + k by Z1, FINSEQ_3:25, NAT_1:10;
A6: v . d = [y,s] by A3, TARSKI:def 1;
j <= len q by A4, FINSEQ_3:25;
then ( <*k*> ^ d in dom (o -term q) & (o -term q) . (<*k*> ^ d) = v . d ) by A2, A5, TREES_4:11, TREES_4:12, NAT_1:13;
then [y,s] in rng (o -term q) by A6, FUNCT_1:def 3;
then y in proj1 (rng (o -term q)) by XTUPLE_0:def 12;
then y in V \/ (proj1 (rng (o -term q))) by XBOOLE_0:def 3;
hence contradiction by A0, XBOOLE_0:def 5; :: thesis:

end;

then reconsider C9 = o -term q1 as context of y by Th53;
take y ; :: thesis:
take C9 ; :: thesis:
take q1 ; :: thesis:
y nin V \/ (proj1 (rng (o -term q))) by A0, XBOOLE_0:def 5;
hence y nin V by XBOOLE_0:def 3; :: thesis:
thus C9 = o -term q1 ; :: thesis:
thus q1 = q +* (m,(y -term)) ; :: thesis:
thus q1 is y -context_including by A1; :: thesis:
A7: q1 . m = y -term by Z0, FUNCT_7:31;
hence m = y -context_pos_in q1 by A1, CPI; :: thesis:
hence y -context_in q1 = y -term by A1, A7, Th71; :: thesis: