let S1, S2 be non empty non void ManySortedSign ; :: thesis:
let X be non-empty ManySortedSet of the carrier of S2; :: thesis:
let f be Function of the carrier of S1, the carrier of S2; :: thesis:
let g be one-to-one Function; :: thesis:
set A = (FreeMSA X) | (S1,f,g);
set H = hom (f,g,X,S1,S2);
defpred S₁[ set ] means ex t1 being Term of S1,(X * f) st
( t1 = $1 & ( for t2 being Term of S1,(X * f) st the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 holds
t1 = t2 ) );
A1: FreeMSA (X * f) = MSAlgebra(# (FreeSort (X * f)),(FreeOper (X * f)) #) by MSAFREE:def 14;
assume A2: f,g form_morphism_between S1,S2 ; :: thesis:
then reconsider h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
reconsider B = (FreeMSA X) | (S1,f,g) as non-empty MSAlgebra over S1 by A2, Th22;
reconsider H9 = hom (f,g,X,S1,S2) as ManySortedFunction of (FreeMSA (X * f)),B ;
A3: for o being OperSymbol of S1
for p being ArgumentSeq of Sym (o,(X * f)) st ( for t being Term of S1,(X * f) st t in rng p holds
S₁[t] ) holds
S₁[[o, the carrier of S1] -tree p]

proof

let o be OperSymbol of S1; :: thesis:
let p be ArgumentSeq of Sym (o,(X * f)); :: thesis:
assume A4: for t being Term of S1,(X * f) st t in rng p holds
S₁[t] ; :: thesis:
A5: dom p = dom (the_arity_of o) by MSATERM:22;
reconsider a = p as Element of Args (o,(FreeMSA (X * f))) by Th1;
A6: [(h . o), the carrier of S2] in [: the carrier' of S2,{ the carrier of S2}:] by ZFMISC_1:106;
reconsider q = (hom (f,g,X,S1,S2)) # a as Element of Args ((h . o),(FreeMSA X)) by A2, Th24;
take t1 = (Sym (o,(X * f))) -tree p; :: thesis:
thus A7: t1 = [o, the carrier of S1] -tree p by MSAFREE:def 9; :: thesis:
reconsider b = q as ArgumentSeq of Sym ((h . o),X) by Th1;
let t2 be Term of S1,(X * f); :: thesis:
assume A8: ( the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 ) ; :: thesis:
the_sort_of t1 = the_result_sort_of o by MSATERM:20;
then A9: ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = [(g . o), the carrier of S2] -tree q by A2, A7, Th40;
( ((Sym ((h . o),X)) -tree b) . {} = Sym ((h . o),X) & Sym ((h . o),X) = [(h . o), the carrier of S2] ) by MSAFREE:def 9, TREES_4:def 4;
then [(h . o), the carrier of S2] -tree b is CompoundTerm of S2,X by A6, MSATERM:def 6;
then t2 is CompoundTerm of S1,X * f by A2, A8, A9, Th41;
then t2 . {} in [: the carrier' of S1,{ the carrier of S1}:] by MSATERM:def 6;
then consider o9, s9 being object such that
A10: o9 in the carrier' of S1 and
A11: ( s9 in { the carrier of S1} & t2 . {} = [o9,s9] ) by ZFMISC_1:def 2;
reconsider o9 = o9 as OperSymbol of S1 by A10;
A12: t2 . {} = [o9, the carrier of S1] by A11, TARSKI:def 1;
then consider r being ArgumentSeq of Sym (o9,(X * f)) such that
A13: t2 = [o9, the carrier of S1] -tree r by MSATERM:10;
reconsider c = r as Element of Args (o9,(FreeMSA (X * f))) by Th1;
reconsider R = (hom (f,g,X,S1,S2)) # c as Element of Args ((h . o9),(FreeMSA X)) by A2, Th24;
the_result_sort_of o9 = the_sort_of t2 by A12, MSATERM:17;
then A14: ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = [(g . o9), the carrier of S2] -tree R by A2, A8, A13, Th40;
then [(g . o9), the carrier of S2] = [(g . o), the carrier of S2] by A9, TREES_4:15;
then h . o = h . o9 by XTUPLE_0:1;
then A15: o = o9 by FUNCT_2:19;
then A16: dom r = dom (the_arity_of o) by MSATERM:22;
A17: q = R by A9, A14, TREES_4:15;

now :: thesis:

let i be Nat; :: thesis:
A18: R = H9 # c ;
assume A19: i in dom (the_arity_of o) ; :: thesis:
then reconsider w1 = p . i, w2 = r . i as Term of S1,(X * f) by A5, A16, MSATERM:22;
A20: the_sort_of w1 = (the_arity_of o) /. i by A5, A19, MSATERM:23;
q = H9 # a ;
then q . i = ((hom (f,g,X,S1,S2)) . (the_sort_of w1)) . w1 by A5, A19, A20, MSUALG_3:def 6;
then A21: ((hom (f,g,X,S1,S2)) . (the_sort_of w1)) . w1 = ((hom (f,g,X,S1,S2)) . (the_sort_of w1)) . w2 by A17, A15, A16, A19, A20, A18, MSUALG_3:def 6;
w1 in rng p by A5, A19, FUNCT_1:def 3;
then A22: S₁[w1] by A4;
the_sort_of w2 = (the_arity_of o) /. i by A15, A16, A19, MSATERM:23;
hence p . i = r . i by A22, A20, A21; :: thesis:

end;

hence t1 = t2 by A7, A13, A15, A5, A16, FINSEQ_1:13; :: thesis:

end;

thus hom (f,g,X,S1,S2) is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) by A2, Def5; :: according to MSUALG_3:def 9 :: thesis:
let i be set ; :: according to MSUALG_3:def 2 :: thesis:
let h be Function; :: thesis:
assume i in dom (hom (f,g,X,S1,S2)) ; :: thesis:
then reconsider s = i as SortSymbol of S1 by PARTFUN1:def 2;
assume A23: (hom (f,g,X,S1,S2)) . i = h ; :: thesis:
then A24: dom h = dom (H9 . s)
.= (FreeSort (X * f)) . s by A1, FUNCT_2:def 1
.= FreeSort ((X * f),s) by MSAFREE:def 11 ;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume A25: ( x in dom h & y in dom h ) ; :: thesis:
FreeSort ((X * f),s) c= S1 -Terms (X * f) by MSATERM:12;
then reconsider t1 = x, t2 = y as Term of S1,(X * f) by A24, A25;
A26: for s being SortSymbol of S1
for v being Element of (X * f) . s holds S₁[ root-tree [v,s]]

proof

let s be SortSymbol of S1; :: thesis:
let v be Element of (X * f) . s; :: thesis:
reconsider t1 = root-tree [v,s] as Term of S1,(X * f) by MSATERM:4;
take t1 ; :: thesis:
thus t1 = root-tree [v,s] ; :: thesis:
let t2 be Term of S1,(X * f); :: thesis:
assume that
A27: the_sort_of t1 = the_sort_of t2 and
A28: ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 ; :: thesis:
A29: the_sort_of t1 = s by MSATERM:14;
A30: ((hom (f,g,X,S1,S2)) . s) . (root-tree [v,s]) = root-tree [v,(f . s)] by A2, Def5;

now :: thesis:

assume t2 . {} in [: the carrier' of S1,{ the carrier of S1}:] ; :: thesis:
then t2 is CompoundTerm of S1,X * f by MSATERM:def 6;
then ( (root-tree [v,(f . s)]) . {} = [v,(f . s)] & root-tree [v,(f . s)] is CompoundTerm of S2,X ) by A2, A27, A28, A30, A29, Th41, TREES_4:3;
then [v,(f . s)] in [: the carrier' of S2,{ the carrier of S2}:] by MSATERM:def 6;
then A31: f . s = the carrier of S2 by ZFMISC_1:106;
f . s in the carrier of S2 ;
hence contradiction by A31; :: thesis:

end;

then consider s2 being SortSymbol of S1, v2 being Element of (X * f) . s2 such that
A32: t2 . {} = [v2,s2] by MSATERM:2;
A33: t2 = root-tree [v2,s2] by A32, MSATERM:5;
then A34: s = s2 by A27, A29, MSATERM:14;
then ((hom (f,g,X,S1,S2)) . s) . t2 = root-tree [v2,(f . s)] by A2, A33, Def5;
then [v,(f . s)] = [v2,(f . s)] by A28, A30, A29, TREES_4:4;
hence t1 = t2 by A33, A34, XTUPLE_0:1; :: thesis:

end;

for t being Term of S1,(X * f) holds S₁[t] from MSATERM:sch 1(A26, A3);
then A35: S₁[t1] ;
( the_sort_of t1 = s & the_sort_of t2 = s ) by A24, A25, MSATERM:def 5;
hence ( not h . x = h . y or x = y ) by A23, A35; :: thesis: