let S be non empty non void ManySortedSign ; 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 b2,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for v being Element of (Free (S,Y))
for h2 being b3 -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; for Y being infinite-yielding ManySortedSet of the carrier of S
for y being Element of Y . s
for Q being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for v being Element of (Free (S,Y))
for h2 being b2 -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; 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 b1 -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; 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; 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)); 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; ( Q is struct-invariant & v is y -omitting implies h2 . v is y -omitting )
assume Z0:
Q is struct-invariant
; ( not v is y -omitting or h2 . v is y -omitting )
defpred S1[ 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 S1[y -term ]
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
S1[v] ) holds
S1[o -term q]
proof
let o be
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
S1[v] ) holds
S1[o -term q]let q be
Element of
Args (
o,
(Free (S,Y)));
( ( for v being Element of (Free (S,Y)) st v in rng q holds
S1[v] ) implies S1[o -term q] )
assume Z3:
for
v being
Element of
(Free (S,Y)) st
v in rng q holds
S1[
v]
;
S1[o -term q]
assume Z4:
o -term q is
y -omitting
;
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;
( 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)
;
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;
verum
end;
hence
h2 . (o -term q) is
y -omitting
by Z0, A4, Th77;
verum
end;
thus
S1[v]
from MSAFREE5:sch 2(A1, A2); verum