( dom f = the carrier of S1 & rng f c= the carrier of S2 )
by A1, PUA2MSS1:def 13;
then reconsider f9 = f as Function of the carrier of S1,the carrier of S2 by FUNCT_2:def 1, RELSET_1:11;
A2:
rng g c= the carrier' of S2
by A1, PUA2MSS1:def 13;
A3:
dom g = the carrier' of S1
by A1, PUA2MSS1:def 13;
then reconsider g9 = g as Function of the carrier' of S1,the carrier' of S2 by A2, FUNCT_2:4;
dom the Charact of A = the carrier' of S2
by PARTFUN1:def 4;
then
dom (the Charact of A * g9) = the carrier' of S1
by A3, A2, RELAT_1:46;
then reconsider C = the Charact of A * g9 as ManySortedSet of the carrier' of S1 by PARTFUN1:def 4;
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
set ;
PBOOLE:def 18 ( 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:7;
A5:
g . o in rng g
by A3, A4, FUNCT_1:def 5;
then reconsider p2 = the
Arity of
S2 . (g . o) as
Element of the
carrier of
S2 * by A2, FUNCT_2:7;
reconsider o =
o as
OperSymbol of
S1 by A4;
A6:
C . o = the
Charact of
A . (g9 . o)
by A2, A4, A5, FUNCT_2:21;
(the Sorts of A * f9) * the
ResultSort of
S1 =
the
Sorts of
A * (f9 * the ResultSort of S1)
by RELAT_1:55
.=
the
Sorts of
A * (the ResultSort of S2 * g)
by A1, PUA2MSS1:def 13
.=
(the Sorts of A * the ResultSort of S2) * g
by RELAT_1:55
;
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:21;
A8:
(the Sorts of A * f9) * p1 =
the
Sorts of
A * (f9 * p1)
by RELAT_1:55
.=
the
Sorts of
A * p2
by A1, A4, PUA2MSS1:def 13
;
(((the Sorts of A * f9) # ) * the Arity of S1) . o =
((the Sorts of A * f9) # ) . p1
by A4, FUNCT_2:21
.=
product ((the Sorts of A * f9) * p1)
by PBOOLE:def 19
.=
(the Sorts of A # ) . p2
by A8, PBOOLE:def 19
.=
((the Sorts of A # ) * the Arity of S2) . (g9 . o)
by A2, A5, FUNCT_2:21
;
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 18;
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