let I be non empty set ; for A being set
for B being V2() ManySortedSet of I
for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
let A be set ; for B being V2() ManySortedSet of I
for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
let B be V2() ManySortedSet of I; for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
let F be ManySortedFunction of I --> A,B; dom (commute F) = A
A1:
dom B = I
by PARTFUN1:def 2;
A2:
dom F = I
by PARTFUN1:def 2;
per cases
( A is empty or not A is empty )
;
suppose A6:
not
A is
empty
;
dom (commute F) = A
rng F c= Funcs (
A,
(union (rng B)))
proof
let x be
object ;
TARSKI:def 3 ( not x in rng F or x in Funcs (A,(union (rng B))) )
assume
x in rng F
;
x in Funcs (A,(union (rng B)))
then consider i being
object such that A7:
i in dom F
and A8:
x = F . i
by FUNCT_1:def 3;
(I --> A) . i = A
by A2, A7, FUNCOP_1:7;
then reconsider x9 =
x as
Function of
A,
(B . i) by A2, A7, A8, PBOOLE:def 15;
B . i in rng B
by A1, A2, A7, FUNCT_1:def 3;
then
(
rng x9 c= B . i &
B . i c= union (rng B) )
by RELAT_1:def 19, ZFMISC_1:74;
then A9:
rng x9 c= union (rng B)
;
dom x9 = A
by A2, A7, FUNCT_2:def 1;
hence
x in Funcs (
A,
(union (rng B)))
by A9, FUNCT_2:def 2;
verum
end; then
F in Funcs (
I,
(Funcs (A,(union (rng B)))))
by A2, FUNCT_2:def 2;
then
commute F in Funcs (
A,
(Funcs (I,(union (rng B)))))
by A6, FUNCT_6:55;
then A10:
commute F is
Function of
A,
(Funcs (I,(union (rng B))))
by FUNCT_2:66;
not
union (rng B) is
empty
by Th2;
then
not
Funcs (
I,
(union (rng B))) is
empty
by FUNCT_2:8;
hence
dom (commute F) = A
by A10, FUNCT_2:def 1;
verum end; end;