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

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