let S be non empty non void ManySortedSign ; :: thesis:
let s be SortSymbol of S; :: thesis:
let o be OperSymbol of S; :: thesis:
let X be non-empty ManySortedSet of the carrier of S; :: thesis:
let x be Element of X . s; :: thesis:
let p be Element of Args (o,(Free (S,X))); :: thesis:
set I = {[x,s]};
set k = p;
reconsider J = [o, the carrier of S] as set ;
s in the carrier of S ;
then s <> the carrier of S ;
then [o, the carrier of S] <> [x,s] by XTUPLE_0:1;
then [o, the carrier of S] nin {[x,s]} by TARSKI:def 1;
then IFIN (J,{[x,s]},{{}},{}) = {} by MATRIX_7:def 1;
then A5: (o -term p) " {[x,s]} = {} \/ (union { (<*i*> ^^ ((p . (i + 1)) " {[x,s]})) where i is Nat : i < len p } ) by Th80;
thus ( p is x -context_including implies o -term p is context of x ) :: thesis:

proof

given i being Nat such that A6: ( i in dom p & p . i is context of x & ( for j being Nat
for t being Element of (Free (S,X)) st j in dom p & j <> i & t = p . j holds
t is x -omitting ) ) ; :: according to MSAFREE5:def 24 :: thesis:
reconsider C = p . i as context of x by A6;
card (Coim (C,[x,s])) = 1 by CONTEXT;
then consider a being object such that
A9: C " {[x,s]} = {a} by CARD_2:42;
a in C " {[x,s]} by A9, TARSKI:def 1;
then reconsider a = a as FinSequence ;
consider j being Nat such that
A7: i = 1 + j by A6, FINSEQ_3:25, NAT_1:10;
1 + j <= len p by A6, A7, FINSEQ_3:25;
then A8: j < len p by NAT_1:13;
union { (<*i*> ^^ ((p . (i + 1)) " {[x,s]})) where i is Nat : i < len p } = {(<*j*> ^ a)}

proof

thus union { (<*i*> ^^ ((p . (i + 1)) " {[x,s]})) where i is Nat : i < len p } c= {(<*j*> ^ a)} :: according to XBOOLE_0:def 10 :: thesis:

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in union { (<*i*> ^^ ((p . (i + 1)) " {[x,s]})) where i is Nat : i < len p } ; :: thesis:
then consider J being set such that
B1: ( b in J & J in { (<*i*> ^^ ((p . (i + 1)) " {[x,s]})) where i is Nat : i < len p } ) by TARSKI:def 4;
consider n being Nat such that
B2: ( J = <*n*> ^^ ((p . (n + 1)) " {[x,s]}) & n < len p ) by B1;
B4: ( 1 <= n + 1 & n + 1 <= len p ) by B2, NAT_1:11, NAT_1:13;
then n + 1 in dom p by FINSEQ_3:25;
then reconsider t = p . (n + 1) as Element of (Free (S,X)) by FUNCT_1:102;

per cases ;

suppose n = j ; :: thesis:

hence b in {(<*j*> ^ a)} by B1, B2, A9, A7, Th6; :: thesis:

end;

suppose n <> j ; :: thesis:

then n + 1 <> j + 1 ;
then t is x -omitting by A6, A7, B4, FINSEQ_3:25;
hence b in {(<*j*> ^ a)} by B1, B2; :: thesis:

end;

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in {(<*j*> ^ a)} ; :: thesis:
then ( b in <*j*> ^^ (C " {[x,s]}) & <*j*> ^^ (C " {[x,s]}) in { (<*i*> ^^ ((p . (i + 1)) " {[x,s]})) where i is Nat : i < len p } ) by A7, A8, A9, Th6;
hence b in union { (<*i*> ^^ ((p . (i + 1)) " {[x,s]})) where i is Nat : i < len p } by TARSKI:def 4; :: thesis:

end;

then card (Coim ((o -term p),[x,s])) = 1 by A5, CARD_1:30;
hence o -term p is context of x by CONTEXT; :: thesis:

end;

assume o -term p is context of x ; :: thesis:
then card (Coim ((o -term p),[x,s])) = 1 by CONTEXT;
then consider a being object such that
D1: Coim ((o -term p),[x,s]) = {a} by CARD_2:42;
a in (o -term p) " {[x,s]} by D1, TARSKI:def 1;
then consider J being set such that
D2: ( a in J & J in { (<*i*> ^^ ((p . (i + 1)) " {[x,s]})) where i is Nat : i < len p } ) by A5, TARSKI:def 4;
consider i being Nat such that
D3: ( J = <*i*> ^^ ((p . (i + 1)) " {[x,s]}) & i < len p ) by D2;
consider p being Element of (p . (i + 1)) " {[x,s]} such that
D4: ( a = <*i*> ^ p & p in (p . (i + 1)) " {[x,s]} ) by D2, D3;
take n = i + 1; :: according to MSAFREE5:def 24 :: thesis:
( 1 <= n & n <= len p ) by D3, NAT_1:11, NAT_1:13;
hence n in dom p by FINSEQ_3:25; :: thesis:
then reconsider kn = p . n as Element of (Free (S,X)) by FUNCT_1:102;
D6: {p} c= kn " {[x,s]} by D4, ZFMISC_1:31;
( J c= {a} & {a} = <*i*> ^^ {p} ) by A5, D1, D2, D4, Th6, ZFMISC_1:74;
then kn " {[x,s]} c= {p} by D3, Th18;
then kn " {[x,s]} = {p} by D6, XBOOLE_0:def 10;
then card (Coim (kn,[x,s])) = 1 by CARD_1:30;
hence p . n is context of x by CONTEXT; :: thesis:
let j be Nat; :: thesis:
let t be Element of (Free (S,X)); :: thesis:
assume D7: ( j in dom p & j <> n & t = p . j ) ; :: thesis:
assume Coim (t,[x,s]) <> {} ; :: according to MSAFREE5:def 21 :: thesis:
then consider c being object such that
D8: c in Coim (t,[x,s]) by XBOOLE_0:7;
reconsider c = c as Node of t by D8, FUNCT_1:def 7;
consider m being Nat such that
D9: j = 1 + m by D7, FINSEQ_3:25, NAT_1:10;
1 + m <= len p by D7, D9, FINSEQ_3:25;
then m < len p by NAT_1:13;
then ( <*m*> ^ c in <*m*> ^^ (t " {[x,s]}) & <*m*> ^^ (t " {[x,s]}) in { (<*i*> ^^ ((p . (i + 1)) " {[x,s]})) where i is Nat : i < len p } ) by D7, D8, D9;
then <*m*> ^ c in {a} by A5, D1, TARSKI:def 4;
then <*m*> ^ c = <*i*> ^ p by D4, TARSKI:def 1;
then ( m = (<*m*> ^ c) . 1 & (<*m*> ^ c) . 1 = i ) by FINSEQ_1:41;
hence contradiction by D7, D9; :: thesis: