let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for t being Element of (Free (S,X)) st x1 <> x2 & t is x2 -omitting holds
(Hom ((Free (S,X)),x1,x2)) . t is x1 -omitting
let s be SortSymbol of S; for X being V5() ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for t being Element of (Free (S,X)) st x1 <> x2 & t is x2 -omitting holds
(Hom ((Free (S,X)),x1,x2)) . t is x1 -omitting
let X be V5() ManySortedSet of the carrier of S; for x1, x2 being Element of X . s
for t being Element of (Free (S,X)) st x1 <> x2 & t is x2 -omitting holds
(Hom ((Free (S,X)),x1,x2)) . t is x1 -omitting
let x1, x2 be Element of X . s; for t being Element of (Free (S,X)) st x1 <> x2 & t is x2 -omitting holds
(Hom ((Free (S,X)),x1,x2)) . t is x1 -omitting
let t be Element of (Free (S,X)); ( x1 <> x2 & t is x2 -omitting implies (Hom ((Free (S,X)),x1,x2)) . t is x1 -omitting )
assume A0:
x1 <> x2
; ( not t is x2 -omitting or (Hom ((Free (S,X)),x1,x2)) . t is x1 -omitting )
set T = Free (S,X);
set h = Hom ((Free (S,X)),x1,x2);
set s0 = s;
defpred S1[ Element of (Free (S,X))] means ( $1 is x2 -omitting implies (Hom ((Free (S,X)),x1,x2)) . $1 is x1 -omitting );
A1:
for s being SortSymbol of S
for x being Element of X . s holds S1[x -term ]
proof
let s be
SortSymbol of
S;
for x being Element of X . s holds S1[x -term ]let x be
Element of
X . s;
S1[x -term ]
set r =
x -term ;
assume Z1:
x -term is
x2 -omitting
;
(Hom ((Free (S,X)),x1,x2)) . (x -term) is x1 -omitting
per cases
( s <> s or ( x1 <> x & x2 <> x ) or ( s = s & x1 = x ) or ( s = s & x2 = x ) )
;
suppose A2:
(
s <> s or (
x1 <> x &
x2 <> x ) )
;
(Hom ((Free (S,X)),x1,x2)) . (x -term) is x1 -omitting then
(
((Hom ((Free (S,X)),x1,x2)) . s) . (x -term) = x -term &
the_sort_of (@ (x -term)) = the_sort_of (x -term) )
by HOM;
then
(
((Hom ((Free (S,X)),x1,x2)) . (the_sort_of (x -term))) . (x -term) = x -term &
x -term is
x1 -omitting )
by A2, SORT, ThC1;
hence
(Hom ((Free (S,X)),x1,x2)) . (x -term) is
x1 -omitting
by ABBR;
verum end; suppose
(
s = s &
x1 = x )
;
(Hom ((Free (S,X)),x1,x2)) . (x -term) is x1 -omitting then
(
((Hom ((Free (S,X)),x1,x2)) . s) . (x -term) = x2 -term &
the_sort_of (@ (x -term)) = the_sort_of (x -term) )
by HOM;
then A4:
((Hom ((Free (S,X)),x1,x2)) . (the_sort_of (x -term))) . (x -term) = x2 -term
by SORT;
x2 -term is
x1 -omitting
by A0, ThC1;
hence
(Hom ((Free (S,X)),x1,x2)) . (x -term) is
x1 -omitting
by A4, ABBR;
verum end; end;
end;
A2:
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) holds
S1[o -term p]
proof
let o be
OperSymbol of
S;
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) holds
S1[o -term p]let p be
Element of
Args (
o,
(Free (S,X)));
( ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) implies S1[o -term p] )
set r =
o -term p;
assume Z2:
for
t being
Element of
(Free (S,X)) st
t in rng p holds
S1[
t]
;
S1[o -term p]
assume S4:
o -term p is
x2 -omitting
;
(Hom ((Free (S,X)),x1,x2)) . (o -term p) is x1 -omitting
A6:
the_sort_of (o -term p) = the_result_sort_of o
by Th8;
reconsider q =
p as
Element of
Args (
o,
(Free (S,X))) ;
reconsider m =
(Hom ((Free (S,X)),x1,x2)) # q as
Element of
Args (
o,
(Free (S,X))) ;
A7:
(
(Den (o,(Free (S,X)))) . q = (Den (o,(Free (S,X)))) . p &
(Den (o,(Free (S,X)))) . p = o -term p )
by MSAFREE4:13;
A9:
((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) . (o -term p) =
(Den (o,(Free (S,X)))) . m
by A7, MSUALG_3:def 7, MSUALG_6:def 2
.=
o -term m
by MSAFREE4:13
;
now for i being Nat st i in dom m holds
m /. i is x1 -omitting let i be
Nat;
( i in dom m implies m /. i is x1 -omitting )assume B1:
i in dom m
;
m /. i is x1 -omitting B2:
(
dom m = dom (the_arity_of o) &
dom (the_arity_of o) = dom p )
by MSUALG_3:6;
then B3:
(
p . i in rng p &
p /. i = p . i &
p . i = q /. i )
by B1, FUNCT_1:def 3, PARTFUN1:def 6;
q /. i in the
Sorts of
(Free (S,X)) . ((the_arity_of o) /. i)
by B1, B2, B3, MSUALG_6:2;
then B5:
the_sort_of (q /. i) = (the_arity_of o) /. i
by SORT;
(
m /. i = m . i &
m . i = ((Hom ((Free (S,X)),x1,x2)) . ((the_arity_of o) /. i)) . (q /. i) )
by B1, PARTFUN1:def 6, B2, B3, MSUALG_3:def 6;
then
(
(Hom ((Free (S,X)),x1,x2)) . (q /. i) = m /. i &
p /. i is
x2 -omitting )
by B1, B2, S4, B5, ABBR, Th54;
hence
m /. i is
x1 -omitting
by B3, Z2;
verum end;
then
o -term m is
x1 -omitting
by Th54;
hence
(Hom ((Free (S,X)),x1,x2)) . (o -term p) is
x1 -omitting
by A6, A9, ABBR;
verum
end;
thus
S1[t]
from MSAFREE5:sch 2(A1, A2); verum