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 of 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 of 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 of 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 of 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 of 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 set ; :: according to PBOOLE:def 18 :: 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 ;
( (h * f) . s = h . fs & the Sorts of A1 . fs = (the Sorts of A1 * f) . s & the Sorts of A2 . fs = (the Sorts of A2 * f) . s & 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, FUNCT_2:21;
hence (h * f) . x is Element of bool [:(the Sorts of (A1 | S1,f,g) . x),(the Sorts of (A2 | S1,f,g) . x):] ; :: thesis: verum