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