( dom f = the carrier of S1 & rng f c= the carrier of S2 )
by A1;

then reconsider f9 = f as Function of the carrier of S1, the carrier of S2 by FUNCT_2:def 1, RELSET_1:4;

A2: rng g c= the carrier' of S2 by A1;

A3: dom g = the carrier' of S1 by A1;

then reconsider g9 = g as Function of the carrier' of S1, the carrier' of S2 by A2, FUNCT_2:2;

dom the Charact of A = the carrier' of S2 by PARTFUN1:def 2;

then dom ( the Charact of A * g9) = the carrier' of S1 by A3, A2, RELAT_1:27;

then reconsider C = the Charact of A * g9 as ManySortedSet of the carrier' of S1 by PARTFUN1:def 2;

C is ManySortedFunction of (( the Sorts of A * f9) #) * the Arity of S1,( the Sorts of A * f9) * the ResultSort of S1

take MSAlgebra(# ( the Sorts of A * f9),C #) ; :: thesis: ( the Sorts of MSAlgebra(# ( the Sorts of A * f9),C #) = the Sorts of A * f & the Charact of MSAlgebra(# ( the Sorts of A * f9),C #) = the Charact of A * g )

thus ( the Sorts of MSAlgebra(# ( the Sorts of A * f9),C #) = the Sorts of A * f & the Charact of MSAlgebra(# ( the Sorts of A * f9),C #) = the Charact of A * g ) ; :: thesis: verum

then reconsider f9 = f as Function of the carrier of S1, the carrier of S2 by FUNCT_2:def 1, RELSET_1:4;

A2: rng g c= the carrier' of S2 by A1;

A3: dom g = the carrier' of S1 by A1;

then reconsider g9 = g as Function of the carrier' of S1, the carrier' of S2 by A2, FUNCT_2:2;

dom the Charact of A = the carrier' of S2 by PARTFUN1:def 2;

then dom ( the Charact of A * g9) = the carrier' of S1 by A3, A2, RELAT_1:27;

then reconsider C = the Charact of A * g9 as ManySortedSet of the carrier' of S1 by PARTFUN1:def 2;

C is ManySortedFunction of (( the Sorts of A * f9) #) * the Arity of S1,( the Sorts of A * f9) * the ResultSort of S1

proof

then reconsider C = C as ManySortedFunction of (( the Sorts of A * f9) #) * the Arity of S1,( the Sorts of A * f9) * the ResultSort of S1 ;
let o be object ; :: according to PBOOLE:def 15 :: thesis: ( not o in the carrier' of S1 or C . o is Element of bool [:(((( the Sorts of A * f9) #) * the Arity of S1) . o),((( the Sorts of A * f9) * the ResultSort of S1) . o):] )

assume A4: o in the carrier' of S1 ; :: thesis: C . o is Element of bool [:(((( the Sorts of A * f9) #) * the Arity of S1) . o),((( the Sorts of A * f9) * the ResultSort of S1) . o):]

then reconsider p1 = the Arity of S1 . o as Element of the carrier of S1 * by FUNCT_2:5;

A5: g . o in rng g by A3, A4, FUNCT_1:def 3;

then reconsider p2 = the Arity of S2 . (g . o) as Element of the carrier of S2 * by A2, FUNCT_2:5;

reconsider o = o as OperSymbol of S1 by A4;

A6: C . o = the Charact of A . (g9 . o) by A2, A4, A5, FUNCT_2:15;

( the Sorts of A * f9) * the ResultSort of S1 = the Sorts of A * (f9 * the ResultSort of S1) by RELAT_1:36

.= the Sorts of A * ( the ResultSort of S2 * g) by A1

.= ( the Sorts of A * the ResultSort of S2) * g by RELAT_1:36 ;

then A7: (( the Sorts of A * f9) * the ResultSort of S1) . o = ( the Sorts of A * the ResultSort of S2) . (g9 . o) by A2, A4, A5, FUNCT_2:15;

A8: ( the Sorts of A * f9) * p1 = the Sorts of A * (f9 * p1) by RELAT_1:36

.= the Sorts of A * p2 by A1, A4 ;

((( the Sorts of A * f9) #) * the Arity of S1) . o = (( the Sorts of A * f9) #) . p1 by A4, FUNCT_2:15

.= product (( the Sorts of A * f9) * p1) by FINSEQ_2:def 5

.= ( the Sorts of A #) . p2 by A8, FINSEQ_2:def 5

.= (( the Sorts of A #) * the Arity of S2) . (g9 . o) by A2, A5, FUNCT_2:15 ;

hence C . o is Element of bool [:(((( the Sorts of A * f9) #) * the Arity of S1) . o),((( the Sorts of A * f9) * the ResultSort of S1) . o):] by A2, A5, A7, A6, PBOOLE:def 15; :: thesis: verum

end;assume A4: o in the carrier' of S1 ; :: thesis: C . o is Element of bool [:(((( the Sorts of A * f9) #) * the Arity of S1) . o),((( the Sorts of A * f9) * the ResultSort of S1) . o):]

then reconsider p1 = the Arity of S1 . o as Element of the carrier of S1 * by FUNCT_2:5;

A5: g . o in rng g by A3, A4, FUNCT_1:def 3;

then reconsider p2 = the Arity of S2 . (g . o) as Element of the carrier of S2 * by A2, FUNCT_2:5;

reconsider o = o as OperSymbol of S1 by A4;

A6: C . o = the Charact of A . (g9 . o) by A2, A4, A5, FUNCT_2:15;

( the Sorts of A * f9) * the ResultSort of S1 = the Sorts of A * (f9 * the ResultSort of S1) by RELAT_1:36

.= the Sorts of A * ( the ResultSort of S2 * g) by A1

.= ( the Sorts of A * the ResultSort of S2) * g by RELAT_1:36 ;

then A7: (( the Sorts of A * f9) * the ResultSort of S1) . o = ( the Sorts of A * the ResultSort of S2) . (g9 . o) by A2, A4, A5, FUNCT_2:15;

A8: ( the Sorts of A * f9) * p1 = the Sorts of A * (f9 * p1) by RELAT_1:36

.= the Sorts of A * p2 by A1, A4 ;

((( the Sorts of A * f9) #) * the Arity of S1) . o = (( the Sorts of A * f9) #) . p1 by A4, FUNCT_2:15

.= product (( the Sorts of A * f9) * p1) by FINSEQ_2:def 5

.= ( the Sorts of A #) . p2 by A8, FINSEQ_2:def 5

.= (( the Sorts of A #) * the Arity of S2) . (g9 . o) by A2, A5, FUNCT_2:15 ;

hence C . o is Element of bool [:(((( the Sorts of A * f9) #) * the Arity of S1) . o),((( the Sorts of A * f9) * the ResultSort of S1) . o):] by A2, A5, A7, A6, PBOOLE:def 15; :: thesis: verum

take MSAlgebra(# ( the Sorts of A * f9),C #) ; :: thesis: ( the Sorts of MSAlgebra(# ( the Sorts of A * f9),C #) = the Sorts of A * f & the Charact of MSAlgebra(# ( the Sorts of A * f9),C #) = the Charact of A * g )

thus ( the Sorts of MSAlgebra(# ( the Sorts of A * f9),C #) = the Sorts of A * f & the Charact of MSAlgebra(# ( the Sorts of A * f9),C #) = the Charact of A * g ) ; :: thesis: verum