let A, B be non empty set ; :: thesis: for C being non-empty 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 non-empty ManySortedSet of A; :: thesis: 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; :: thesis: 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; :: thesis: 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:] :: according to XBOOLE_0:def 10 :: thesis: [:A,B:] c= dom (uncurry InpFs)

proof

let i be object ; :: 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 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; :: thesis: verum

end;

let i1, i2 be object ; :: according to RELAT_1:def 3 :: thesis: ( 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:] ; :: thesis: [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; :: thesis: 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 ; :: thesis: ( c = (commute InpFs) . b & c in C )
thus c = (commute InpFs) . b ; :: thesis: c in C
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in A or c . i in C . i )
reconsider h = InpFs . i as Function ;
assume A10: i in A ; :: thesis: 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; :: thesis: verum