( 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
proof
let o be
object ;
PBOOLE:def 15 ( 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
;
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;
verum
end;
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 ;
take
MSAlgebra(# ( the Sorts of A * f9),C #)
; ( 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 )
; verum