let S be non empty non void ManySortedSign ; :: thesis: 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 t being Element of (Free (S,X)) st t in rng p holds
t 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 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 t being Element of (Free (S,X)) st t in rng p holds
t is x -omitting ) iff o -term p is x -omitting )
let o be OperSymbol of S; :: thesis: 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 t being Element of (Free (S,X)) st t in rng p holds
t is x -omitting ) iff o -term p is x -omitting )
let X be V5() 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 t being Element of (Free (S,X)) st t in rng p holds
t 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 t being Element of (Free (S,X)) st t in rng p holds
t is x -omitting ) iff o -term p is x -omitting )
let p be Element of Args (o,(Free (S,X))); :: thesis: ( ( for t being Element of (Free (S,X)) st t in rng p holds
t is x -omitting ) iff o -term p is x -omitting )
A0: now :: thesis: ( ( for i being Nat st i in dom p holds
p /. i is x -omitting ) implies for t being Element of (Free (S,X)) st t in rng p holds
t is x -omitting )
assume A1: for i being Nat st i in dom p holds
p /. i is x -omitting ; :: thesis: for t being Element of (Free (S,X)) st t in rng p holds
t is x -omitting
let t be Element of (Free (S,X)); :: thesis: ( t in rng p implies t is x -omitting )
assume t in rng p ; :: thesis: t is x -omitting
then consider i being object such that
A2: ( i in dom p & t = p . i ) by FUNCT_1:def 3;
reconsider i = i as Nat by A2;
t = p /. i by A2, PARTFUN1:def 6;
hence t is x -omitting by A1, A2; :: thesis: verum
end;
now :: thesis: ( ( for t being Element of (Free (S,X)) st t in rng p holds
t is x -omitting ) implies for i being Nat st i in dom p holds
p /. i is x -omitting )
assume A3: for t being Element of (Free (S,X)) st t in rng p holds
t is x -omitting ; :: 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 i in dom p ; :: thesis: p /. i is x -omitting
then ( p /. i = p . i & p . i in rng p ) by FUNCT_1:def 3, PARTFUN1:def 6;
hence p /. i is x -omitting by A3; :: thesis: verum
end;
hence ( ( for t being Element of (Free (S,X)) st t in rng p holds
t is x -omitting ) iff o -term p is x -omitting ) by A0, Th54; :: thesis: verum