let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for T being b2,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st T is struct-invariant & x1 <> x2 & r is x2 -omitting holds
(Hom (T,x1,x2)) . r is x1 -omitting
let s be SortSymbol of S; :: thesis: for X being V5() ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st T is struct-invariant & x1 <> x2 & r is x2 -omitting holds
(Hom (T,x1,x2)) . r is x1 -omitting
let X be V5() ManySortedSet of the carrier of S; :: thesis: for x1, x2 being Element of X . s
for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st T is struct-invariant & x1 <> x2 & r is x2 -omitting holds
(Hom (T,x1,x2)) . r is x1 -omitting
let x1, x2 be Element of X . s; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st T is struct-invariant & x1 <> x2 & r is x2 -omitting holds
(Hom (T,x1,x2)) . r is x1 -omitting
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for r being Element of T st T is struct-invariant & x1 <> x2 & r is x2 -omitting holds
(Hom (T,x1,x2)) . r is x1 -omitting
let r be Element of T; :: thesis: ( T is struct-invariant & x1 <> x2 & r is x2 -omitting implies (Hom (T,x1,x2)) . r is x1 -omitting )
assume that
AA: for o being OperSymbol of S
for p being Element of Args (o,T) st (Den (o,T)) . p = (Den (o,(Free (S,X)))) . p holds
for s being SortSymbol of S
for x1, x2 being Element of X . s holds (Den (o,T)) . ((Hom (T,x1,x2)) # p) = (Den (o,(Free (S,X)))) . ((Hom (T,x1,x2)) # p) and
A0: x1 <> x2 ; :: according to MSAFREE5:def 32 :: thesis: ( not r is x2 -omitting or (Hom (T,x1,x2)) . r is x1 -omitting )
set h = Hom (T,x1,x2);
set s0 = s;
defpred S1[ Element of T] means ( $1 is x2 -omitting implies (Hom (T,x1,x2)) . $1 is x1 -omitting );
A1: for s being SortSymbol of S
for x being Element of X . s
for r being Element of T st r = x -term holds
S1[r]
proof
let s be SortSymbol of S; :: thesis: for x being Element of X . s
for r being Element of T st r = x -term holds
S1[r]
let x be Element of X . s; :: thesis: for r being Element of T st r = x -term holds
S1[r]
let r be Element of T; :: thesis: ( r = x -term implies S1[r] )
assume Z0: r = x -term ; :: thesis: S1[r]
assume Z1: r is x2 -omitting ; :: thesis: (Hom (T,x1,x2)) . r 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 (T,x1,x2)) . r is x1 -omitting
then ( ((Hom (T,x1,x2)) . s) . r = r & the_sort_of (@ r) = the_sort_of r ) by Z0, HOM, Lem00;
then ( ((Hom (T,x1,x2)) . (the_sort_of r)) . r = r & x -term is x1 -omitting ) by A2, Z0, SORT, ThC1;
hence (Hom (T,x1,x2)) . r is x1 -omitting by Z0, ABBR; :: thesis: verum
end;
suppose ( s = s & x1 = x ) ; :: thesis: (Hom (T,x1,x2)) . r is x1 -omitting
then ( ((Hom (T,x1,x2)) . s) . r = x2 -term & the_sort_of (@ r) = the_sort_of r ) by Z0, HOM, Lem00;
then A4: ((Hom (T,x1,x2)) . (the_sort_of r)) . r = x2 -term by Z0, SORT;
x2 -term is x1 -omitting by A0, ThC1;
hence (Hom (T,x1,x2)) . r is x1 -omitting by A4, ABBR; :: thesis: verum
end;
suppose A3: ( s = s & x2 = x ) ; :: thesis: (Hom (T,x1,x2)) . r is x1 -omitting
not x2 -term is x2 -omitting ;
hence (Hom (T,x1,x2)) . r is x1 -omitting by Z0, Z1, A3; :: thesis: verum
end;
end;
end;
A2: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X)))
for r being Element of T st r = o -term p & ( for t being Element of T st t in rng p holds
S1[t] ) holds
S1[r]
proof
let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X)))
for r being Element of T st r = o -term p & ( for t being Element of T st t in rng p holds
S1[t] ) holds
S1[r]
let p be Element of Args (o,(Free (S,X))); :: thesis: for r being Element of T st r = o -term p & ( for t being Element of T st t in rng p holds
S1[t] ) holds
S1[r]
let r be Element of T; :: thesis: ( r = o -term p & ( for t being Element of T st t in rng p holds
S1[t] ) implies S1[r] )
assume Z1: r = o -term p ; :: thesis: ( ex t being Element of T st
( t in rng p & not S1[t] ) or S1[r] )
assume Z2: for t being Element of T st t in rng p holds
S1[t] ; :: thesis: S1[r]
assume r is x2 -omitting ; :: thesis: (Hom (T,x1,x2)) . r is x1 -omitting
then S3: o -term p is x2 -omitting by Z1;
the_sort_of (@ r) = the_sort_of r by Lem00;
then A6: the_sort_of r = the_result_sort_of o by Z1, Th8;
then o -term p in the Sorts of T . (the_result_sort_of o) by Z1, SORT;
then A5: (Den (o,(Free (S,X)))) . p in the Sorts of T . (the_result_sort_of o) by MSAFREE4:13;
then reconsider q = p as Element of Args (o,T) by MSAFREE4:def 8;
Args (o,T) c= Args (o,(Free (S,X))) by MSAFREE4:41;
then reconsider m = (Hom (T,x1,x2)) # q as Element of Args (o,(Free (S,X))) ;
A7: ( (Den (o,T)) . q = (Den (o,(Free (S,X)))) . p & (Den (o,(Free (S,X)))) . p = o -term p ) by A5, MSAFREE4:def 8, MSAFREE4:13;
A9: ((Hom (T,x1,x2)) . (the_result_sort_of o)) . r = (Den (o,T)) . ((Hom (T,x1,x2)) # q) by Z1, A7, MSUALG_3:def 7, MSUALG_6:def 2
.= (Den (o,(Free (S,X)))) . m by AA, A7
.= 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;
then B4: S1[q /. i] by Z2;
q /. i in the Sorts of T . ((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 (T,x1,x2)) . ((the_arity_of o) /. i)) . (q /. i) ) by B1, PARTFUN1:def 6, B2, B3, MSUALG_3:def 6;
then ( (Hom (T,x1,x2)) . (q /. i) = m /. i & p /. i is x2 -omitting ) by B1, B2, S3, B5, ABBR, Th54;
hence m /. i is x1 -omitting by B3, B4, OMIT; :: thesis: verum
end;
then o -term m is x1 -omitting by Th54;
hence (Hom (T,x1,x2)) . r is x1 -omitting by A9, A6, ABBR; :: thesis: verum
end;
thus S1[r] from MSAFREE5:sch 3(A1, A2); :: thesis: verum