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 b2,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st T is struct-invariant holds
for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = ((Hom ((Free (S,X)),x1,x2)) . s) . 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 b1,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st T is struct-invariant holds
for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = ((Hom ((Free (S,X)),x1,x2)) . s) . 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 st T is struct-invariant holds
for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = ((Hom ((Free (S,X)),x1,x2)) . s) . 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 st T is struct-invariant holds
for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = ((Hom ((Free (S,X)),x1,x2)) . s) . r
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: ( T is struct-invariant implies for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = ((Hom ((Free (S,X)),x1,x2)) . s) . r )
assume 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) ; :: according to MSAFREE5:def 32 :: thesis: for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = ((Hom ((Free (S,X)),x1,x2)) . s) . r
set h = Hom (T,x1,x2);
set g = Hom ((Free (S,X)),x1,x2);
defpred S1[ Element of T] means ((Hom (T,x1,x2)) . (the_sort_of $1)) . $1 = ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of $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
S1[r]
proof
let s1 be SortSymbol of S; :: thesis: for x being Element of X . s1
for r being Element of T st r = x -term holds
S1[r]
let x11 be Element of X . s1; :: thesis: for r being Element of T st r = x11 -term holds
S1[r]
let r be Element of T; :: thesis: ( r = x11 -term implies S1[r] )
assume A2: r = x11 -term ; :: thesis: S1[r]
then A3: ( the_sort_of r = the_sort_of (@ r) & the_sort_of (@ r) = s1 ) by SORT, Lem00;
per cases ( ( s = s1 & x11 = x1 ) or ( s = s1 & x11 = x2 ) or s <> s1 or ( x11 <> x1 & x11 <> x2 ) ) ;
suppose ( s = s1 & x11 = x1 ) ; :: thesis: S1[r]
then ( ((Hom (T,x1,x2)) . s1) . r = x2 -term & ((Hom ((Free (S,X)),x1,x2)) . s1) . r = x2 -term ) by A2, HOM;
hence S1[r] by A3; :: thesis: verum
end;
suppose ( s = s1 & x11 = x2 ) ; :: thesis: S1[r]
then ( ((Hom (T,x1,x2)) . s1) . r = x1 -term & ((Hom ((Free (S,X)),x1,x2)) . s1) . r = x1 -term ) by A2, HOM;
hence S1[r] by A3; :: thesis: verum
end;
suppose ( s <> s1 or ( x11 <> x1 & x11 <> x2 ) ) ; :: thesis: S1[r]
then ( ((Hom (T,x1,x2)) . s1) . r = r & ((Hom ((Free (S,X)),x1,x2)) . s1) . r = r ) by A2, HOM;
hence S1[r] by A3; :: thesis: verum
end;
end;
end;
A4: 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 Z0: r = o -term p ; :: thesis: ( ex t being Element of T st
( t in rng p & not S1[t] ) or S1[r] )
assume Z1: for t being Element of T st t in rng p holds
S1[t] ; :: thesis: S1[r]
A6: r = (Den (o,(Free (S,X)))) . p by Z0, MSAFREE4:13;
A7: ( r in the Sorts of T . (the_sort_of r) & the_sort_of r = the_sort_of (@ r) & the_sort_of (@ r) = the_result_sort_of o ) by Z0, SORT, Lem00;
then reconsider q = p as Element of Args (o,T) by A6, MSAFREE4:def 8;
r = (Den (o,T)) . q by A6, A7, MSAFREE4:def 8;
then A8: (Den (o,T)) . ((Hom (T,x1,x2)) # q) = (Den (o,(Free (S,X)))) . ((Hom (T,x1,x2)) # q) by AA, A6;
(Hom ((Free (S,X)),x1,x2)) # p = (Hom (T,x1,x2)) # q
proof
B1: ( dom ((Hom ((Free (S,X)),x1,x2)) # p) = dom (the_arity_of o) & dom (the_arity_of o) = dom ((Hom (T,x1,x2)) # q) ) by MSUALG_3:6;
hence len ((Hom ((Free (S,X)),x1,x2)) # p) = len ((Hom (T,x1,x2)) # q) by FINSEQ_3:29; :: according to FINSEQ_1:def 18 :: thesis: for b1 being set holds
( not 1 <= b1 or not b1 <= len ((Hom ((Free (S,X)),x1,x2)) # p) or ((Hom ((Free (S,X)),x1,x2)) # p) . b1 = ((Hom (T,x1,x2)) # q) . b1 )
let i be Nat; :: thesis: ( not 1 <= i or not i <= len ((Hom ((Free (S,X)),x1,x2)) # p) or ((Hom ((Free (S,X)),x1,x2)) # p) . i = ((Hom (T,x1,x2)) # q) . i )
assume C0: ( 1 <= i & i <= len ((Hom ((Free (S,X)),x1,x2)) # p) ) ; :: thesis: ((Hom ((Free (S,X)),x1,x2)) # p) . i = ((Hom (T,x1,x2)) # q) . i
then C1: i in dom ((Hom ((Free (S,X)),x1,x2)) # p) by FINSEQ_3:25;
C3: dom p = dom (the_arity_of o) by MSUALG_6:2;
then C5: ( q /. i = q . i & q . i in the Sorts of T . ((the_arity_of o) /. i) ) by C0, B1, PARTFUN1:def 6, FINSEQ_3:25, MSUALG_6:2;
then C4: ( the_sort_of (q /. i) = (the_arity_of o) /. i & p . i in rng p ) by B1, C1, C3, SORT, FUNCT_1:def 3;
thus ((Hom ((Free (S,X)),x1,x2)) # p) . i = ((Hom ((Free (S,X)),x1,x2)) . ((the_arity_of o) /. i)) . (q /. i) by C0, C3, C5, B1, FINSEQ_3:25, MSUALG_3:def 6
.= ((Hom (T,x1,x2)) . ((the_arity_of o) /. i)) . (q /. i) by C4, C5, Z1
.= ((Hom (T,x1,x2)) # q) . i by C0, C3, C5, B1, FINSEQ_3:25, MSUALG_3:def 6 ; :: thesis: verum
end;
then ((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) . r = (Den (o,(Free (S,X)))) . ((Hom (T,x1,x2)) # q) by A6, MSUALG_6:def 2, MSUALG_3:def 7
.= ((Hom (T,x1,x2)) . (the_result_sort_of o)) . ((Den (o,T)) . q) by A8, MSUALG_6:def 2, MSUALG_3:def 7
.= ((Hom (T,x1,x2)) . (the_result_sort_of o)) . r by A6, A7, MSAFREE4:def 8 ;
hence S1[r] by A7; :: thesis: verum
end;
let r be Element of T,s; :: thesis: ((Hom (T,x1,x2)) . s) . r = ((Hom ((Free (S,X)),x1,x2)) . s) . r
A9: S1[r] from MSAFREE5:sch 3(A1, A4);
the_sort_of r = s by SORT;
hence ((Hom (T,x1,x2)) . s) . r = ((Hom ((Free (S,X)),x1,x2)) . s) . r by A9; :: thesis: verum