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)) . (the_result_sort_of o)) . ([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)) . (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 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)) . (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, Th24;
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;
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 Th3
.= (Den ((h . o),(FreeMSA X))) . q by A1, Th23
.= [(g . o), the carrier of S2] -tree q by A3, Th3 ;
:: thesis: verum