let S1, S2 be non empty non void ManySortedSign ; 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; 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; 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; ( 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
; 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; 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))); 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; ( 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
; ((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
;
verum