let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for T being b₂,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st r is x1 -omitting & r is x2 -omitting holds
(Hom (T,x1,x2)) . r = r
let s be SortSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st r is x1 -omitting & r is x2 -omitting holds
(Hom (T,x1,x2)) . r = r
let X be non-empty 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 r is x1 -omitting & r is x2 -omitting holds
(Hom (T,x1,x2)) . r = r
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 r is x1 -omitting & r is x2 -omitting holds
(Hom (T,x1,x2)) . r = r
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 r is x1 -omitting & r is x2 -omitting holds
(Hom (T,x1,x2)) . r = r
let r be Element of T; :: thesis: ( r is x1 -omitting & r is x2 -omitting implies (Hom (T,x1,x2)) . r = r )
set s0 = s;
defpred S₁[ Element of T] means ( $1 is x1 -omitting & $1 is x2 -omitting implies ((Hom (T,x1,x2)) . (the_sort_of $1)) . $1 = $1 );
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
S₁[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
S₁[r]
let x be Element of X . s; :: thesis: for r being Element of T st r = x -term holds
S₁[r]
let r be Element of T; :: thesis: ( r = x -term implies S₁[r] )
assume Z0: r = x -term ; :: thesis: S₁[r]
assume ( r is x1 -omitting & r is x2 -omitting ) ; :: thesis: ((Hom (T,x1,x2)) . (the_sort_of r)) . r = r
then ( x -term is x1 -omitting & x -term is x2 -omitting ) by Z0;
then ( ( s <> s or x <> x1 ) & ( s <> s or x <> x2 ) ) ;
then ( ((Hom (T,x1,x2)) . s) . r = r & the_sort_of (@ r) = the_sort_of r ) by Z0, HOM, Lem00;
hence ((Hom (T,x1,x2)) . (the_sort_of r)) . r = r by Z0, SORT; :: thesis: verum

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
S₁[t] ) holds
S₁[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
S₁[t] ) holds
S₁[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
S₁[t] ) holds
S₁[r]
let r be Element of T; :: thesis: ( r = o -term p & ( for t being Element of T st t in rng p holds
S₁[t] ) implies S₁[r] )
assume Z1: r = o -term p ; :: thesis: ( ex t being Element of T st
( t in rng p & not S₁[t] ) or S₁[r] )
assume Z2: for t being Element of T st t in rng p holds
S₁[t] ; :: thesis: S₁[r]
assume ( r is x1 -omitting & r is x2 -omitting ) ; :: thesis: ((Hom (T,x1,x2)) . (the_sort_of r)) . r = r
then Z4: ( o -term p is x1 -omitting & o -term p is x2 -omitting ) by Z1;
A9: the_sort_of (@ r) = the_sort_of r by Lem00;
then 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;
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;
A8: ((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;
q = (Hom (T,x1,x2)) # q

proof

B1: ( dom q = dom (the_arity_of o) & dom (the_arity_of o) = dom ((Hom (T,x1,x2)) # q) ) by MSUALG_3:6;
hence len q = len ((Hom (T,x1,x2)) # q) by FINSEQ_3:29; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len q or q . b₁ = ((Hom (T,x1,x2)) # q) . b₁ )
let i be Nat; :: thesis: ( not 1 <= i or not i <= len q or q . i = ((Hom (T,x1,x2)) # q) . i )
assume B5: ( 1 <= i & i <= len q ) ; :: thesis: q . i = ((Hom (T,x1,x2)) # q) . i
then B4: i in dom q by FINSEQ_3:25;
then B2: ( p /. i is x1 -omitting & p /. i is x2 -omitting & p /. i = p . i & p . i = q /. i & p . i in rng p ) by Z4, Th54, FUNCT_1:def 3, PARTFUN1:def 6;
then ( q /. i is x1 -omitting & q /. i is x2 -omitting ) ;
then B3: ((Hom (T,x1,x2)) . (the_sort_of (q /. i))) . (q /. i) = q /. i by Z2, B2;
q /. i in the Sorts of T . ((the_arity_of o) /. i) by B1, B5, B2, FINSEQ_3:25, MSUALG_6:2;
then the_sort_of (q /. i) = (the_arity_of o) /. i by SORT;
hence q . i = ((Hom (T,x1,x2)) # q) . i by B4, B2, B3, MSUALG_3:def 6; :: thesis: verum

end;

hence ((Hom (T,x1,x2)) . (the_sort_of r)) . r = r by Z1, A9, A7, A8, Th8; :: thesis: verum

end;

S₁[r] from MSAFREE5:sch 3(A1, A2);
hence ( r is x1 -omitting & r is x2 -omitting implies (Hom (T,x1,x2)) . r = r ) by ABBR; :: thesis: verum