let A, B be non empty set ; :: thesis: 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; :: 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:]

( (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

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; :: 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

then A9:
( commute InpFs = curry' (uncurry InpFs) & ex g being Function st
thus
dom (uncurry InpFs) c= [:A,B:]
:: according to XBOOLE_0:def 10 :: thesis: [:A,B:] c= 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;proof

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) )
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;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

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

( (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