let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for o being OperSymbol of S
for X being V5() 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; for o being OperSymbol of S
for X being V5() 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; for X being V5() 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 V5() 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 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 p be Element of Args (o,(Free (S,X))); ( ( 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 ( 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
;
o -term p is x -omitting thus
o -term p is
x -omitting
verumproof
assume
Coim (
(o -term p),
[x,s])
<> {}
;
MSAFREE5:def 21 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;
verum
end;
end;
assume B1:
Coim ((o -term p),[x,s]) = {}
; MSAFREE5:def 21 for i being Nat st i in dom p holds
p /. i is x -omitting
let i be Nat; ( i in dom p implies p /. i is x -omitting )
assume B2:
i in dom p
; 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]) = {}
; MSAFREE5:def 21 verum