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