let S1, S2 be non empty non void ManySortedSign ; :: thesis: for X being V2() ManySortedSet of the carrier of S2

for f being Function of the carrier of S1, the carrier of S2

for g being one-to-one Function st f,g form_morphism_between S1,S2 holds

hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)

let X be V2() ManySortedSet of the carrier of S2; :: thesis: for f being Function of the carrier of S1, the carrier of S2

for g being one-to-one Function st f,g form_morphism_between S1,S2 holds

hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)

let f be Function of the carrier of S1, the carrier of S2; :: thesis: for g being one-to-one Function st f,g form_morphism_between S1,S2 holds

hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)

let g be one-to-one Function; :: thesis: ( f,g form_morphism_between S1,S2 implies hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) )

set A = (FreeMSA X) | (S1,f,g);

set H = hom (f,g,X,S1,S2);

defpred S_{1}[ 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: hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)

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_{1}[t] ) holds

S_{1}[[o, the carrier of S1] -tree p]

let i be set ; :: according to MSUALG_3:def 2 :: thesis: for b_{1} being set holds

( not i in dom (hom (f,g,X,S1,S2)) or not (hom (f,g,X,S1,S2)) . i = b_{1} or b_{1} is one-to-one )

let h be Function; :: thesis: ( not i in dom (hom (f,g,X,S1,S2)) or not (hom (f,g,X,S1,S2)) . i = h or h is one-to-one )

assume i in dom (hom (f,g,X,S1,S2)) ; :: thesis: ( not (hom (f,g,X,S1,S2)) . i = h or h is one-to-one )

then reconsider s = i as SortSymbol of S1 by PARTFUN1:def 2;

assume A23: (hom (f,g,X,S1,S2)) . i = h ; :: thesis: h is one-to-one

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: ( not x in dom h or not y in dom h or not h . x = h . y or x = y )

assume A25: ( x in dom h & y in dom h ) ; :: thesis: ( not h . x = h . y or x = y )

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_{1}[ root-tree [v,s]]
_{1}[t]
from MSATERM:sch 1(A26, A3);

then A35: S_{1}[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: verum

for f being Function of the carrier of S1, the carrier of S2

for g being one-to-one Function st f,g form_morphism_between S1,S2 holds

hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)

let X be V2() ManySortedSet of the carrier of S2; :: thesis: for f being Function of the carrier of S1, the carrier of S2

for g being one-to-one Function st f,g form_morphism_between S1,S2 holds

hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)

let f be Function of the carrier of S1, the carrier of S2; :: thesis: for g being one-to-one Function st f,g form_morphism_between S1,S2 holds

hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)

let g be one-to-one Function; :: thesis: ( f,g form_morphism_between S1,S2 implies hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) )

set A = (FreeMSA X) | (S1,f,g);

set H = hom (f,g,X,S1,S2);

defpred S

( 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: hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)

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

S

proof

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: hom (f,g,X,S1,S2) is "1-1"
let o be OperSymbol of S1; :: thesis: 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_{1}[t] ) holds

S_{1}[[o, the carrier of S1] -tree p]

let p be ArgumentSeq of Sym (o,(X * f)); :: thesis: ( ( for t being Term of S1,(X * f) st t in rng p holds

S_{1}[t] ) implies S_{1}[[o, the carrier of S1] -tree p] )

assume A4: for t being Term of S1,(X * f) st t in rng p holds

S_{1}[t]
; :: thesis: S_{1}[[o, the carrier of S1] -tree p]

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: ( t1 = [o, the carrier of S1] -tree p & ( 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 ) )

thus A7: t1 = [o, the carrier of S1] -tree p by MSAFREE:def 9; :: thesis: 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

reconsider b = q as ArgumentSeq of Sym ((h . o),X) by Th1;

let t2 be Term of S1,(X * f); :: thesis: ( 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 implies t1 = t2 )

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: t1 = t2

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;

end;S

S

let p be ArgumentSeq of Sym (o,(X * f)); :: thesis: ( ( for t being Term of S1,(X * f) st t in rng p holds

S

assume A4: for t being Term of S1,(X * f) st t in rng p holds

S

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: ( t1 = [o, the carrier of S1] -tree p & ( 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 ) )

thus A7: t1 = [o, the carrier of S1] -tree p by MSAFREE:def 9; :: thesis: 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

reconsider b = q as ArgumentSeq of Sym ((h . o),X) by Th1;

let t2 be Term of S1,(X * f); :: thesis: ( 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 implies t1 = t2 )

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: t1 = t2

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: for i being Nat st i in dom (the_arity_of o) holds

p . i = r . i

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

let i be Nat; :: thesis: ( i in dom (the_arity_of o) implies p . i = r . i )

A18: R = H9 # c ;

assume A19: i in dom (the_arity_of o) ; :: thesis: p . i = r . i

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_{1}[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: verum

end;A18: R = H9 # c ;

assume A19: i in dom (the_arity_of o) ; :: thesis: p . i = r . i

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

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: verum

let i be set ; :: according to MSUALG_3:def 2 :: thesis: for b

( not i in dom (hom (f,g,X,S1,S2)) or not (hom (f,g,X,S1,S2)) . i = b

let h be Function; :: thesis: ( not i in dom (hom (f,g,X,S1,S2)) or not (hom (f,g,X,S1,S2)) . i = h or h is one-to-one )

assume i in dom (hom (f,g,X,S1,S2)) ; :: thesis: ( not (hom (f,g,X,S1,S2)) . i = h or h is one-to-one )

then reconsider s = i as SortSymbol of S1 by PARTFUN1:def 2;

assume A23: (hom (f,g,X,S1,S2)) . i = h ; :: thesis: h is one-to-one

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: ( not x in dom h or not y in dom h or not h . x = h . y or x = y )

assume A25: ( x in dom h & y in dom h ) ; :: thesis: ( not h . x = h . y or x = y )

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

proof

for t being Term of S1,(X * f) holds S
let s be SortSymbol of S1; :: thesis: for v being Element of (X * f) . s holds S_{1}[ root-tree [v,s]]

let v be Element of (X * f) . s; :: thesis: S_{1}[ root-tree [v,s]]

reconsider t1 = root-tree [v,s] as Term of S1,(X * f) by MSATERM:4;

take t1 ; :: thesis: ( t1 = root-tree [v,s] & ( 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 ) )

thus t1 = root-tree [v,s] ; :: thesis: 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

let t2 be Term of S1,(X * f); :: thesis: ( 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 implies t1 = t2 )

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: t1 = t2

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;

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: verum

end;let v be Element of (X * f) . s; :: thesis: S

reconsider t1 = root-tree [v,s] as Term of S1,(X * f) by MSATERM:4;

take t1 ; :: thesis: ( t1 = root-tree [v,s] & ( 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 ) )

thus t1 = root-tree [v,s] ; :: thesis: 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

let t2 be Term of S1,(X * f); :: thesis: ( 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 implies t1 = t2 )

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: t1 = t2

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: not t2 . {} in [: the carrier' of S1,{ the carrier of S1}:]

then consider s2 being SortSymbol of S1, v2 being Element of (X * f) . s2 such that assume
t2 . {} in [: the carrier' of S1,{ the carrier of S1}:]
; :: thesis: contradiction

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: verum

end;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: verum

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: verum

then A35: S

( 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: verum