let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for U1, U2 being MSAlgebra of S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args o,U1 <> {} holds
Args o,U2 <> {}
let o be OperSymbol of S; :: thesis: for U1, U2 being MSAlgebra of S st the Sorts of U1 is_transformable_to the Sorts of U2 & Args o,U1 <> {} holds
Args o,U2 <> {}
let U1, U2 be MSAlgebra of S; :: thesis: ( the Sorts of U1 is_transformable_to the Sorts of U2 & Args o,U1 <> {} implies Args o,U2 <> {} )
A2:
dom the Arity of S = the carrier' of S
by FUNCT_2:def 1;
then A3: ((the Sorts of U1 # ) * the Arity of S) . o =
(the Sorts of U1 # ) . (the Arity of S . o)
by FUNCT_1:23
.=
(the Sorts of U1 # ) . (the_arity_of o)
by MSUALG_1:def 6
;
assume A4:
( the Sorts of U1 is_transformable_to the Sorts of U2 & Args o,U1 <> {} )
; :: thesis: Args o,U2 <> {}
then
((the Sorts of U1 # ) * the Arity of S) . o <> {}
by MSUALG_1:def 9;
then
product (the Sorts of U1 * (the_arity_of o)) <> {}
by A3, PBOOLE:def 19;
then A5:
not {} in rng (the Sorts of U1 * (the_arity_of o))
by CARD_3:37;
dom the Sorts of U1 = the carrier of S
by PARTFUN1:def 4;
then
rng (the_arity_of o) c= dom the Sorts of U1
;
then A6:
dom (the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:46;
A7:
dom (the Sorts of U2 * (the_arity_of o)) c= dom (the_arity_of o)
by RELAT_1:44;
now let x be
set ;
:: thesis: ( x in dom (the Sorts of U2 * (the_arity_of o)) implies (the Sorts of U2 * (the_arity_of o)) . x <> {} )assume A8:
x in dom (the Sorts of U2 * (the_arity_of o))
;
:: thesis: (the Sorts of U2 * (the_arity_of o)) . x <> {} then A9:
(the Sorts of U1 * (the_arity_of o)) . x = the
Sorts of
U1 . ((the_arity_of o) . x)
by A7, FUNCT_1:23;
(the_arity_of o) . x in rng (the_arity_of o)
by A7, A8, FUNCT_1:def 5;
then
( the
Sorts of
U1 . ((the_arity_of o) . x) <> {} implies the
Sorts of
U2 . ((the_arity_of o) . x) <> {} )
by A4, PZFMISC1:def 3;
hence
(the Sorts of U2 * (the_arity_of o)) . x <> {}
by A5, A6, A7, A8, A9, FUNCT_1:23, FUNCT_1:def 5;
:: thesis: verum end;
then
not {} in rng (the Sorts of U2 * (the_arity_of o))
by FUNCT_1:def 5;
then
product (the Sorts of U2 * (the_arity_of o)) <> {}
by CARD_3:37;
then
(the Sorts of U2 # ) . (the_arity_of o) <> {}
by PBOOLE:def 19;
then
(the Sorts of U2 # ) . (the Arity of S . o) <> {}
by MSUALG_1:def 6;
then
((the Sorts of U2 # ) * the Arity of S) . o <> {}
by A2, FUNCT_1:23;
hence
Args o,U2 <> {}
by MSUALG_1:def 9; :: thesis: verum