A2:
( dom g = the carrier' of S1 & rng g c= the carrier' of S2 )
by A1, PUA2MSS1:def 13;
then reconsider g' = g as Function of the carrier' of S1,the carrier' of S2 by FUNCT_2:4;
( dom f = the carrier of S1 & rng f c= the carrier of S2 )
by A1, PUA2MSS1:def 13;
then reconsider f' = f as Function of the carrier of S1,the carrier of S2 by FUNCT_2:def 1, RELSET_1:11;
dom the Charact of A = the carrier' of S2
by PBOOLE:def 3;
then
dom (the Charact of A * g') = the carrier' of S1
by A2, RELAT_1:46;
then reconsider C = the Charact of A * g' as ManySortedSet of the carrier' of S1 by PBOOLE:def 3;
C is ManySortedFunction of ((the Sorts of A * f') # ) * the Arity of S1,(the Sorts of A * f') * the ResultSort of S1
proof
let o be
set ;
:: according to PBOOLE:def 18 :: thesis: ( not o in the carrier' of S1 or C . o is M6((((the Sorts of A * f') # ) * the Arity of S1) . o,((the Sorts of A * f') * the ResultSort of S1) . o) )
assume A3:
o in the
carrier' of
S1
;
:: thesis: C . o is M6((((the Sorts of A * f') # ) * the Arity of S1) . o,((the Sorts of A * f') * the ResultSort of S1) . o)
then reconsider p1 = the
Arity of
S1 . o as
Element of the
carrier of
S1 * by FUNCT_2:7;
A4:
g . o in rng g
by A2, A3, 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 A3;
A5:
(the Sorts of A * f') * p1 =
the
Sorts of
A * (f' * p1)
by RELAT_1:55
.=
the
Sorts of
A * p2
by A1, A3, PUA2MSS1:def 13
;
A6:
(((the Sorts of A * f') # ) * the Arity of S1) . o =
((the Sorts of A * f') # ) . p1
by A3, FUNCT_2:21
.=
product ((the Sorts of A * f') * p1)
by PBOOLE:def 19
.=
(the Sorts of A # ) . p2
by A5, PBOOLE:def 19
.=
((the Sorts of A # ) * the Arity of S2) . (g' . o)
by A2, A4, FUNCT_2:21
;
(the Sorts of A * f') * the
ResultSort of
S1 =
the
Sorts of
A * (f' * 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 * f') * the ResultSort of S1) . o = (the Sorts of A * the ResultSort of S2) . (g' . o)
by A2, A3, A4, FUNCT_2:21;
C . o = the
Charact of
A . (g' . o)
by A2, A3, A4, FUNCT_2:21;
hence
C . o is
M6(
(((the Sorts of A * f') # ) * the Arity of S1) . o,
((the Sorts of A * f') * the ResultSort of S1) . o)
by A2, A4, A6, A7, PBOOLE:def 18;
:: thesis: verum
end;
then reconsider C = C as ManySortedFunction of ((the Sorts of A * f') # ) * the Arity of S1,(the Sorts of A * f') * the ResultSort of S1 ;
take
MSAlgebra(# (the Sorts of A * f'),C #)
; :: thesis: ( the Sorts of MSAlgebra(# (the Sorts of A * f'),C #) = the Sorts of A * f & the Charact of MSAlgebra(# (the Sorts of A * f'),C #) = the Charact of A * g )
thus
( the Sorts of MSAlgebra(# (the Sorts of A * f'),C #) = the Sorts of A * f & the Charact of MSAlgebra(# (the Sorts of A * f'),C #) = the Charact of A * g )
; :: thesis: verum