let A, B be non empty set ; :: thesis: for C being V2() ManySortedSet of
for InpFs being ManySortedFunction of A --> B,C
for b being Element of B ex c being ManySortedSet of st
( c = (commute InpFs) . b & c in C )
let C be V2() ManySortedSet of ; :: thesis: for InpFs being ManySortedFunction of A --> B,C
for b being Element of B ex c being ManySortedSet of st
( c = (commute InpFs) . b & c in C )
let InpFs be ManySortedFunction of A --> B,C; :: thesis: for b being Element of B ex c being ManySortedSet of st
( c = (commute InpFs) . b & c in C )
let b be Element of B; :: thesis: ex c being ManySortedSet of st
( c = (commute InpFs) . b & c in C )
A1:
commute InpFs = curry' (uncurry InpFs)
by FUNCT_6:def 12;
A2:
dom InpFs = A
by PARTFUN1:def 4;
dom (uncurry InpFs) = [:A,B:]
proof
thus
dom (uncurry InpFs) c= [:A,B:]
:: according to XBOOLE_0:def 10 :: thesis: [:A,B:] c= dom (uncurry InpFs)proof
let i be
set ;
:: according to TARSKI:def 3 :: thesis: ( not i in dom (uncurry InpFs) or i in [:A,B:] )
assume
i in dom (uncurry InpFs)
;
:: thesis: i in [:A,B:]
then consider x being
set ,
g being
Function,
y being
set such that A3:
i = [x,y]
and A4:
x in dom InpFs
and A5:
g = InpFs . x
and A6:
y in dom g
by FUNCT_5:def 4;
A7:
C . x <> {}
by A2, A4;
g is
Function of
((A --> B) . x),
(C . x)
by A2, A4, A5, PBOOLE:def 18;
then
dom g = (A --> B) . x
by A7, FUNCT_2:def 1;
then
dom g = B
by A2, A4, FUNCOP_1:13;
hence
i in [:A,B:]
by A2, A3, A4, A6, ZFMISC_1:106;
:: thesis: verum
end;
let i1,
i2 be
set ;
:: according to RELAT_1:def 3 :: thesis: ( not [i1,i2] in [:A,B:] or [i1,i2] in dom (uncurry InpFs) )
assume A8:
[i1,i2] in [:A,B:]
;
:: thesis: [i1,i2] in dom (uncurry InpFs)
then A9:
[i1,i2] = [([i1,i2] `1 ),([i1,i2] `2 )]
by MCART_1:23;
A10:
[i1,i2] `1 in dom InpFs
by A2, A8, MCART_1:10;
reconsider g =
InpFs . ([i1,i2] `1 ) as
Function ;
A11:
C . ([i1,i2] `1 ) <> {}
by A2, A10;
g is
Function of
((A --> B) . ([i1,i2] `1 )),
(C . ([i1,i2] `1 ))
by A8, MCART_1:10, PBOOLE:def 18;
then
dom g = (A --> B) . ([i1,i2] `1 )
by A11, FUNCT_2:def 1;
then
dom g = B
by A8, FUNCOP_1:13, MCART_1:10;
then
[i1,i2] `2 in dom g
by A8, MCART_1:10;
hence
[i1,i2] in dom (uncurry InpFs)
by A9, A10, FUNCT_5:45;
:: thesis: verum
end;
then consider g being Function such that
A12:
( (curry' (uncurry InpFs)) . b = g & dom g = A )
and
rng g c= rng (uncurry InpFs)
and
A13:
for i being set st i in A holds
g . i = (uncurry InpFs) . i,b
by FUNCT_5:39;
reconsider c = (commute InpFs) . b as ManySortedSet of by A1, A12, PARTFUN1:def 4, RELAT_1:def 18;
take
c
; :: thesis: ( c = (commute InpFs) . b & c in C )
thus
c = (commute InpFs) . b
; :: thesis: c in C
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in A or c . i in C . i )
assume A14:
i in A
; :: thesis: c . i in C . i
reconsider h = InpFs . i as Function ;
A15:
C . i <> {}
by A14;
(A --> B) . i = B
by A14, FUNCOP_1:13;
then A16:
h is Function of B,(C . i)
by A14, PBOOLE:def 18;
then A17:
dom h = B
by A15, FUNCT_2:def 1;
c . i =
(uncurry InpFs) . i,b
by A1, A12, A13, A14
.=
h . b
by A2, A14, A17, FUNCT_5:45
;
hence
c . i in C . i
by A15, A16, FUNCT_2:7; :: thesis: verum