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 Function st f,g form_morphism_between S1,S2 holds
for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . ) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q

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 Function st f,g form_morphism_between S1,S2 holds
for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . ) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q

let f be Function of the carrier of S1, the carrier of S2; :: thesis: for g being Function st f,g form_morphism_between S1,S2 holds
for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . ) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q

let g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . ) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q )

set F = hom (f,g,X,S1,S2);
assume A1: f,g form_morphism_between S1,S2 ; :: thesis: for o being OperSymbol of S1
for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . ) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q

then reconsider h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
let o be OperSymbol of S1; :: thesis: for p being Element of Args (o,(FreeMSA (X * f)))
for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . ) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q

let p be Element of Args (o,(FreeMSA (X * f))); :: thesis: for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds
((hom (f,g,X,S1,S2)) . ) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q

let q be FinSequence; :: thesis: ( q = (hom (f,g,X,S1,S2)) # p implies ((hom (f,g,X,S1,S2)) . ) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q )
assume A2: q = (hom (f,g,X,S1,S2)) # p ; :: thesis: ((hom (f,g,X,S1,S2)) . ) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q
then A3: q is Element of Args ((h . o),()) by ;
hom (f,g,X,S1,S2) is_homomorphism FreeMSA (X * f),() | (S1,f,g) by ;
then ((hom (f,g,X,S1,S2)) . ) . ((Den (o,(FreeMSA (X * f)))) . p) = (Den (o,(() | (S1,f,g)))) . q by A2;
hence ((hom (f,g,X,S1,S2)) . ) . ([o, the carrier of S1] -tree p) = (Den (o,(() | (S1,f,g)))) . q by Th3
.= (Den ((h . o),())) . q by
.= [(g . o), the carrier of S2] -tree q by ;
:: thesis: verum