let S1, S2 be non empty ManySortedSign ; :: 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 A1, A2 being MSAlgebra over S2

for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))

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 A1, A2 being MSAlgebra over S2

for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))

let g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies for A1, A2 being MSAlgebra over S2

for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g)) )

assume A1: f,g form_morphism_between S1,S2 ; :: thesis: for A1, A2 being MSAlgebra over S2

for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))

let A1, A2 be MSAlgebra over S2; :: thesis: for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))

let h be ManySortedFunction of the Sorts of A1, the Sorts of A2; :: thesis: h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))

set B1 = A1 | (S1,f,g);

set B2 = A2 | (S1,f,g);

let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in the carrier of S1 or (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):] )

assume x in the carrier of S1 ; :: thesis: (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):]

then reconsider s = x as SortSymbol of S1 ;

reconsider fs = f . s as SortSymbol of S2 ;

A2: ( (h * f) . s = h . fs & the Sorts of A1 . fs = ( the Sorts of A1 * f) . s ) by FUNCT_2:15;

A3: the Sorts of A2 . fs = ( the Sorts of A2 * f) . s by FUNCT_2:15;

( the Sorts of A1 * f = the Sorts of (A1 | (S1,f,g)) & the Sorts of A2 * f = the Sorts of (A2 | (S1,f,g)) ) by A1, Def3;

hence (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):] by A2, A3; :: thesis: verum

for g being Function st f,g form_morphism_between S1,S2 holds

for A1, A2 being MSAlgebra over S2

for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))

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 A1, A2 being MSAlgebra over S2

for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))

let g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies for A1, A2 being MSAlgebra over S2

for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g)) )

assume A1: f,g form_morphism_between S1,S2 ; :: thesis: for A1, A2 being MSAlgebra over S2

for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))

let A1, A2 be MSAlgebra over S2; :: thesis: for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))

let h be ManySortedFunction of the Sorts of A1, the Sorts of A2; :: thesis: h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))

set B1 = A1 | (S1,f,g);

set B2 = A2 | (S1,f,g);

let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in the carrier of S1 or (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):] )

assume x in the carrier of S1 ; :: thesis: (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):]

then reconsider s = x as SortSymbol of S1 ;

reconsider fs = f . s as SortSymbol of S2 ;

A2: ( (h * f) . s = h . fs & the Sorts of A1 . fs = ( the Sorts of A1 * f) . s ) by FUNCT_2:15;

A3: the Sorts of A2 . fs = ( the Sorts of A2 * f) . s by FUNCT_2:15;

( the Sorts of A1 * f = the Sorts of (A1 | (S1,f,g)) & the Sorts of A2 * f = the Sorts of (A2 | (S1,f,g)) ) by A1, Def3;

hence (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):] by A2, A3; :: thesis: verum