let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) holds
( ( for i being Nat st i in dom p holds
p /. i is x -omitting ) iff o -term p is x -omitting )
let s be SortSymbol of S; :: thesis: for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) holds
( ( for i being Nat st i in dom p holds
p /. i is x -omitting ) iff o -term p is x -omitting )
let o be OperSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) holds
( ( for i being Nat st i in dom p holds
p /. i is x -omitting ) iff o -term p is x -omitting )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) holds
( ( for i being Nat st i in dom p holds
p /. i is x -omitting ) iff o -term p is x -omitting )
let x be Element of X . s; :: thesis: for p being Element of Args (o,(Free (S,X))) holds
( ( for i being Nat st i in dom p holds
p /. i is x -omitting ) iff o -term p is x -omitting )
let p be Element of Args (o,(Free (S,X))); :: thesis: ( ( for i being Nat st i in dom p holds
p /. i is x -omitting ) iff o -term p is x -omitting )
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;

hereby :: thesis: ( o -term p is x -omitting implies for i being Nat st i in dom p holds
p /. i is x -omitting )

assume A6: for i being Nat st i in dom p holds
p /. i is x -omitting ; :: thesis: o -term p is x -omitting
thus o -term p is x -omitting :: thesis: verum

proof

assume Coim ((o -term p),[x,s]) <> {} ; :: according to MSAFREE5:def 21 :: thesis: contradiction
then consider a being object such that
A7: a in Coim ((o -term p),[x,s]) by XBOOLE_0:7;
consider J being set such that
A8: ( a in J & J in { (<*i*> ^^ ((p . (i + 1)) " {[x,s]})) where i is Nat : i < len p } ) by A5, A7, TARSKI:def 4;
consider i being Nat such that
A9: ( J = <*i*> ^^ ((p . (i + 1)) " {[x,s]}) & i < len p ) by A8;
( 1 <= i + 1 & i + 1 <= len p ) by A9, NAT_1:11, NAT_1:13;
then ( p /. (i + 1) = p . (i + 1) & p /. (i + 1) is x -omitting ) by A6, FINSEQ_3:25, PARTFUN1:def 6;
hence contradiction by A8, A9; :: thesis: verum

end;

end;

assume B1: Coim ((o -term p),[x,s]) = {} ; :: according to MSAFREE5:def 21 :: thesis: for i being Nat st i in dom p holds
p /. i is x -omitting
let i be Nat; :: thesis: ( i in dom p implies p /. i is x -omitting )
assume B2: i in dom p ; :: thesis: p /. i is x -omitting
then consider j being Nat such that
B3: i = 1 + j by NAT_1:10, FINSEQ_3:25;
1 + j <= len p by B2, B3, FINSEQ_3:25;
then j < len p by NAT_1:13;
then <*j*> ^^ ((p . i) " {[x,s]}) in { (<*i*> ^^ ((p . (i + 1)) " {[x,s]})) where i is Nat : i < len p } by B3;
then ( <*j*> ^^ ((p . i) " {[x,s]}) c= {} & {} = <*j*> ^^ {} ) by A5, B1, ZFMISC_1:74;
then ( (p . i) " {[x,s]} c= {} & p /. i = p . i ) by B2, Th18, PARTFUN1:def 6;
hence Coim ((p /. i),[x,s]) = {} ; :: according to MSAFREE5:def 21 :: thesis: verum