let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for y being Element of Y . s
for Q being b₂,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for v being Element of (Free (S,Y))
for h2 being b₃ -constant Homomorphism of Free (S,Y),Q st Q is struct-invariant & v is y -omitting holds
h2 . v is y -omitting
let s be SortSymbol of S; :: thesis: for Y being infinite-yielding ManySortedSet of the carrier of S
for y being Element of Y . s
for Q being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for v being Element of (Free (S,Y))
for h2 being b₂ -constant Homomorphism of Free (S,Y),Q st Q is struct-invariant & v is y -omitting holds
h2 . v is y -omitting
let Y be infinite-yielding ManySortedSet of the carrier of S; :: thesis: for y being Element of Y . s
for Q being Y,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for v being Element of (Free (S,Y))
for h2 being b₁ -constant Homomorphism of Free (S,Y),Q st Q is struct-invariant & v is y -omitting holds
h2 . v is y -omitting
let y be Element of Y . s; :: thesis: for Q being Y,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for v being Element of (Free (S,Y))
for h2 being y -constant Homomorphism of Free (S,Y),Q st Q is struct-invariant & v is y -omitting holds
h2 . v is y -omitting
let Q be Y,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for v being Element of (Free (S,Y))
for h2 being y -constant Homomorphism of Free (S,Y),Q st Q is struct-invariant & v is y -omitting holds
h2 . v is y -omitting
let v be Element of (Free (S,Y)); :: thesis: for h2 being y -constant Homomorphism of Free (S,Y),Q st Q is struct-invariant & v is y -omitting holds
h2 . v is y -omitting
let h2 be y -constant Homomorphism of Free (S,Y),Q; :: thesis: ( Q is struct-invariant & v is y -omitting implies h2 . v is y -omitting )
assume Z0: Q is struct-invariant ; :: thesis: ( not v is y -omitting or h2 . v is y -omitting )
defpred S₁[ Element of (Free (S,Y))] means ( $1 is y -omitting implies h2 . $1 is y -omitting );
set x0 = y;
set s0 = s;
A1: for s being SortSymbol of S
for y being Element of Y . s holds S₁[y -term ]

proof

let s be SortSymbol of S; :: thesis: for y being Element of Y . s holds S₁[y -term ]
let y be Element of Y . s; :: thesis: S₁[y -term ]
assume y -term is y -omitting ; :: thesis: h2 . (y -term) is y -omitting
then ( y <> y or s <> s ) ;
hence h2 . (y -term) is y -omitting by CNST; :: thesis: verum

end;

A2: for o being OperSymbol of S
for q being Element of Args (o,(Free (S,Y))) st ( for v being Element of (Free (S,Y)) st v in rng q holds
S₁[v] ) holds
S₁[o -term q]

proof

let o be OperSymbol of S; :: thesis: for q being Element of Args (o,(Free (S,Y))) st ( for v being Element of (Free (S,Y)) st v in rng q holds
S₁[v] ) holds
S₁[o -term q]
let q be Element of Args (o,(Free (S,Y))); :: thesis: ( ( for v being Element of (Free (S,Y)) st v in rng q holds
S₁[v] ) implies S₁[o -term q] )
assume Z3: for v being Element of (Free (S,Y)) st v in rng q holds
S₁[v] ; :: thesis: S₁[o -term q]
assume Z4: o -term q is y -omitting ; :: thesis: h2 . (o -term q) is y -omitting
canonical_homomorphism Q is_homomorphism Free (S,Y),Q by MSAFREE4:def 10;
then A3: h2 is_homomorphism Free (S,Y),Q by HOMO;
the_sort_of (o -term q) = the_result_sort_of o by Th8;
then A4: h2 . (o -term q) = (h2 . (the_result_sort_of o)) . (o -term q) by ABBR
.= (h2 . (the_result_sort_of o)) . ((Den (o,(Free (S,Y)))) . q) by MSAFREE4:13
.= (Den (o,Q)) . (h2 # q) by A3, MSUALG_3:def 7 ;
for t being Element of Q st t in rng (h2 # q) holds
t is y -omitting

proof

let t be Element of Q; :: thesis: ( t in rng (h2 # q) implies t is y -omitting )
A5: ( dom q = dom (the_arity_of o) & dom (the_arity_of o) = dom (h2 # q) ) by MSUALG_3:6;
assume t in rng (h2 # q) ; :: thesis: t is y -omitting
then consider i being object such that
A6: ( i in dom q & t = (h2 # q) . i ) by A5, FUNCT_1:def 3;
reconsider i = i as Nat by A6;
A8: q . i = q /. i by A6, PARTFUN1:def 6;
then q /. i in the Sorts of (Free (S,Y)) . ((the_arity_of o) /. i) by A5, A6, MSUALG_6:2;
then A7: the_sort_of (q /. i) = (the_arity_of o) /. i by SORT;
A9: t = (h2 . ((the_arity_of o) /. i)) . (q /. i) by A6, A8, MSUALG_3:def 6
.= h2 . (q /. i) by A7, ABBR ;
( q /. i is y -omitting & q /. i in rng q ) by Z4, A6, A8, Th54, FUNCT_1:def 3;
hence t is y -omitting by A9, Z3; :: thesis: verum

end;

hence h2 . (o -term q) is y -omitting by Z0, A4, Th77; :: thesis: verum

end;

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