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:]
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 ;
then dom g = (A --> B) . x by ;
then dom g = B by ;
hence i in [:A,B:] by ; :: 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 ;
g is Function of ((A --> B) . ([i1,i2] `1)),(C . ([i1,i2] `1)) by ;
then dom g = (A --> B) . ([i1,i2] `1) by ;
then dom g = B by ;
then A8: [i1,i2] `2 in dom g by ;
thus [i1,i2] in dom (uncurry InpFs) by ; :: 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 ;
then reconsider c = (commute InpFs) . b as ManySortedSet of A by ;
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 ;
then A12: dom h = B by ;
c . i = (uncurry InpFs) . (i,b) by
.= h . b by ;
hence c . i in C . i by ; :: thesis: verum