let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for o being OperSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for y being Element of Y . s
for Q being b3,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st Q is struct-invariant holds
for p being Element of Args (o,Q) st ( for t being Element of Q st t in rng p holds
t is y -omitting ) holds
for t being Element of Q st t = (Den (o,Q)) . p holds
t is y -omitting
let s be SortSymbol of S; :: thesis: for o being OperSymbol 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 st Q is struct-invariant holds
for p being Element of Args (o,Q) st ( for t being Element of Q st t in rng p holds
t is y -omitting ) holds
for t being Element of Q st t = (Den (o,Q)) . p holds
t is y -omitting
let o be OperSymbol of S; :: thesis: 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 st Q is struct-invariant holds
for p being Element of Args (o,Q) st ( for t being Element of Q st t in rng p holds
t is y -omitting ) holds
for t being Element of Q st t = (Den (o,Q)) . p holds
t 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 st Q is struct-invariant holds
for p being Element of Args (o,Q) st ( for t being Element of Q st t in rng p holds
t is y -omitting ) holds
for t being Element of Q st t = (Den (o,Q)) . p holds
t 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 st Q is struct-invariant holds
for p being Element of Args (o,Q) st ( for t being Element of Q st t in rng p holds
t is y -omitting ) holds
for t being Element of Q st t = (Den (o,Q)) . p holds
t is y -omitting
let Q be Y,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: ( Q is struct-invariant implies for p being Element of Args (o,Q) st ( for t being Element of Q st t in rng p holds
t is y -omitting ) holds
for t being Element of Q st t = (Den (o,Q)) . p holds
t is y -omitting )
assume ZZ: Q is struct-invariant ; :: thesis: for p being Element of Args (o,Q) st ( for t being Element of Q st t in rng p holds
t is y -omitting ) holds
for t being Element of Q st t = (Den (o,Q)) . p holds
t is y -omitting
let p be Element of Args (o,Q); :: thesis: ( ( for t being Element of Q st t in rng p holds
t is y -omitting ) implies for t being Element of Q st t = (Den (o,Q)) . p holds
t is y -omitting )
assume Z0: for t being Element of Q st t in rng p holds
t is y -omitting ; :: thesis: for t being Element of Q st t = (Den (o,Q)) . p holds
t is y -omitting
let t be Element of Q; :: thesis: ( t = (Den (o,Q)) . p implies t is y -omitting )
assume t = (Den (o,Q)) . p ; :: thesis: t is y -omitting
then A1: t = ((canonical_homomorphism Q) . (the_result_sort_of o)) . ((Den (o,(Free (S,Y)))) . p) by MSAFREE4:67;
Args (o,Q) c= Args (o,(Free (S,Y))) by MSAFREE4:41;
then reconsider q = p as Element of Args (o,(Free (S,Y))) ;
A2: (Den (o,(Free (S,Y)))) . q = o -term q by MSAFREE4:13;
now :: thesis: for v being Element of (Free (S,Y)) st v in rng p holds
v is y -omitting
let v be Element of (Free (S,Y)); :: thesis: ( v in rng p implies v is y -omitting )
assume A5: v in rng p ; :: thesis: v is y -omitting
then reconsider d = v as Element of Q by RELAT_1:167;
d is y -omitting by Z0, A5;
hence v is y -omitting ; :: thesis: verum
end;
then A3: o -term q is y -omitting by Th54A;
the_sort_of (o -term q) = the_result_sort_of o by Th8;
then t = (canonical_homomorphism Q) . (o -term q) by A1, A2, ABBR;
hence t is y -omitting by ZZ, A3, Th68; :: thesis: verum