let S be non empty non void ManySortedSign ; for o being OperSymbol of S
for U1, U2 being MSAlgebra over 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; for U1, U2 being MSAlgebra over 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 over S; ( the Sorts of U1 is_transformable_to the Sorts of U2 & Args (o,U1) <> {} implies Args (o,U2) <> {} )
assume that
A1:
the Sorts of U1 is_transformable_to the Sorts of U2
and
A2:
Args (o,U1) <> {}
; Args (o,U2) <> {}
A3:
(( the Sorts of U1 #) * the Arity of S) . o <> {}
by A2, MSUALG_1:def 4;
dom the Sorts of U1 = the carrier of S
by PARTFUN1:def 2;
then
rng (the_arity_of o) c= dom the Sorts of U1
;
then A4:
dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o)
by RELAT_1:27;
A5:
dom ( the Sorts of U2 * (the_arity_of o)) c= dom (the_arity_of o)
by RELAT_1:25;
A6:
dom the Arity of S = the carrier' of S
by FUNCT_2:def 1;
then (( the Sorts of U1 #) * the Arity of S) . o =
( the Sorts of U1 #) . ( the Arity of S . o)
by FUNCT_1:13
.=
( the Sorts of U1 #) . (the_arity_of o)
by MSUALG_1:def 1
;
then
product ( the Sorts of U1 * (the_arity_of o)) <> {}
by A3, FINSEQ_2:def 5;
then A7:
not {} in rng ( the Sorts of U1 * (the_arity_of o))
by CARD_3:26;
now for x being object st x in dom ( the Sorts of U2 * (the_arity_of o)) holds
( the Sorts of U2 * (the_arity_of o)) . x <> {} let x be
object ;
( 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))
;
( the Sorts of U2 * (the_arity_of o)) . x <> {} then
(the_arity_of o) . x in rng (the_arity_of o)
by A5, FUNCT_1:def 3;
then A9:
( the
Sorts of
U1 . ((the_arity_of o) . x) <> {} implies the
Sorts of
U2 . ((the_arity_of o) . x) <> {} )
by A1, PZFMISC1:def 3;
( the Sorts of U1 * (the_arity_of o)) . x = the
Sorts of
U1 . ((the_arity_of o) . x)
by A5, A8, FUNCT_1:13;
hence
( the Sorts of U2 * (the_arity_of o)) . x <> {}
by A7, A4, A5, A8, A9, FUNCT_1:13, FUNCT_1:def 3;
verum end;
then
not {} in rng ( the Sorts of U2 * (the_arity_of o))
by FUNCT_1:def 3;
then
product ( the Sorts of U2 * (the_arity_of o)) <> {}
by CARD_3:26;
then
( the Sorts of U2 #) . (the_arity_of o) <> {}
by FINSEQ_2:def 5;
then
( the Sorts of U2 #) . ( the Arity of S . o) <> {}
by MSUALG_1:def 1;
then
(( the Sorts of U2 #) * the Arity of S) . o <> {}
by A6, FUNCT_1:13;
hence
Args (o,U2) <> {}
by MSUALG_1:def 4; verum