let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty 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; :: thesis: for X being non-empty 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 non-empty ManySortedSet of the carrier of S; :: thesis: 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; :: thesis: 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)); :: thesis: ( x1 <> x2 & t is x2 -omitting implies (Hom ((Free (S,X)),x1,x2)) . t is x1 -omitting )
assume A0: x1 <> x2 ; :: thesis: ( 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 S₁[ 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 S₁[x -term ]

proof

let s be SortSymbol of S; :: thesis: for x being Element of X . s holds S₁[x -term ]
let x be Element of X . s; :: thesis: S₁[x -term ]
set r = x -term ;
assume Z1: x -term is x2 -omitting ; :: thesis: (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 ) ) ; :: thesis: (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; :: thesis: verum

end;

suppose ( s = s & x1 = x ) ; :: thesis: (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; :: thesis: verum

end;

suppose A3: ( s = s & x2 = x ) ; :: thesis: (Hom ((Free (S,X)),x1,x2)) . (x -term) is x1 -omitting

thus (Hom ((Free (S,X)),x1,x2)) . (x -term) is x1 -omitting by Z1, A3; :: thesis: 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
S₁[t] ) holds
S₁[o -term p]

proof

let o be OperSymbol of S; :: thesis: 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
S₁[t] ) holds
S₁[o -term p]
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
S₁[t] ) implies S₁[o -term p] )
set r = o -term p;
assume Z2: for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ; :: thesis: S₁[o -term p]
assume S4: o -term p is x2 -omitting ; :: thesis: (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 :: thesis: for i being Nat st i in dom m holds
m /. i is x1 -omitting

let i be Nat; :: thesis: ( i in dom m implies m /. i is x1 -omitting )
assume B1: i in dom m ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

thus S₁[t] from MSAFREE5:sch 2(A1, A2); :: thesis: verum