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)) st Q is struct-invariant & v is y -omitting holds
(canonical_homomorphism Q) . 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)) st Q is struct-invariant & v is y -omitting holds
(canonical_homomorphism Q) . 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)) st Q is struct-invariant & v is y -omitting holds
(canonical_homomorphism Q) . 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)) st Q is struct-invariant & v is y -omitting holds
(canonical_homomorphism Q) . 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)) st Q is struct-invariant & v is y -omitting holds
(canonical_homomorphism Q) . v is y -omitting
let v be Element of (Free (S,Y)); :: thesis: ( Q is struct-invariant & v is y -omitting implies (canonical_homomorphism Q) . v is y -omitting )
assume AA: Q is struct-invariant ; :: thesis: ( not v is y -omitting or (canonical_homomorphism Q) . v is y -omitting )
assume Z0: v is y -omitting ; :: thesis: (canonical_homomorphism Q) . v is y -omitting
set H = canonical_homomorphism Q;
assume Z1: not (canonical_homomorphism Q) . v is y -omitting ; :: thesis: contradiction
reconsider Hv = (canonical_homomorphism Q) . v as Element of (Free (S,Y)) by MSAFREE4:39;
consider x being Element of Y . s such that
A1: for v1 being Element of (Free (S,Y)) st v1 in {v,Hv} holds
v1 is x -omitting by Th3A;
( v in {v,Hv} & Hv in {v,Hv} ) by TARSKI:def 2;
then A2: ( v is x -omitting & Hv is x -omitting ) by A1;
then A4: ( x <> y & (canonical_homomorphism Q) . v is x -omitting ) by Z1;
A3: (Hom (Q,x,y)) . ((canonical_homomorphism Q) . v) = ((Hom (Q,x,y)) ** (canonical_homomorphism Q)) . v by Th14
.= ((canonical_homomorphism Q) ** (Hom ((Free (S,Y)),x,y))) . v by Th66
.= (canonical_homomorphism Q) . ((Hom ((Free (S,Y)),x,y)) . v) by Th14
.= (canonical_homomorphism Q) . v by Z0, A2, Th78 ;
Hom (Q,x,y) = Hom (Q,y,x) by Th56;
hence contradiction by Z1, A3, AA, A4, Th79; :: thesis: verum