let S1, S2 be non empty non void ManySortedSign ; :: thesis: for X being V16() 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) . (the_result_sort_of o)) . ([o,the carrier of S1] -tree p) = [(g . o),the carrier of S2] -tree q
let X be V16() 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) . (the_result_sort_of o)) . ([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) . (the_result_sort_of o)) . ([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) . (the_result_sort_of o)) . ([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) . (the_result_sort_of o)) . ([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 Th10;
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) . (the_result_sort_of o)) . ([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) . (the_result_sort_of o)) . ([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) . (the_result_sort_of o)) . ([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) . (the_result_sort_of o)) . ([o,the carrier of S1] -tree p) = [(g . o),the carrier of S2] -tree q
then A3: q is Element of Args (h . o),(FreeMSA X) by A1, Th25;
hom f,g,X,S1,S2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | S1,f,g by A1, Def5;
then ((hom f,g,X,S1,S2) . (the_result_sort_of o)) . ((Den o,(FreeMSA (X * f))) . p) = (Den o,((FreeMSA X) | S1,f,g)) . q by A2, MSUALG_3:def 9;
hence ((hom f,g,X,S1,S2) . (the_result_sort_of o)) . ([o,the carrier of S1] -tree p) = (Den o,((FreeMSA X) | S1,f,g)) . q by Th4
.= (Den (h . o),(FreeMSA X)) . q by A1, Th24
.= [(g . o),the carrier of S2] -tree q by A3, Th4 ;
:: thesis: verum