let X, Y be non empty set ; :: thesis: for Z being non empty RelStr
for S being non empty SubRelStr of Z |^ [:X,Y:]
for T being non empty SubRelStr of (Z |^ Y) |^ X
for f being Function of S,T st f is currying & f is V7() & f is onto holds
f " is uncurrying

let Z be non empty RelStr ; :: thesis: for S being non empty SubRelStr of Z |^ [:X,Y:]
for T being non empty SubRelStr of (Z |^ Y) |^ X
for f being Function of S,T st f is currying & f is V7() & f is onto holds
f " is uncurrying

let S be non empty SubRelStr of Z |^ [:X,Y:]; :: thesis: for T being non empty SubRelStr of (Z |^ Y) |^ X
for f being Function of S,T st f is currying & f is V7() & f is onto holds
f " is uncurrying

let T be non empty SubRelStr of (Z |^ Y) |^ X; :: thesis: for f being Function of S,T st f is currying & f is V7() & f is onto holds
f " is uncurrying

let f be Function of S,T; :: thesis: ( f is currying & f is V7() & f is onto implies f " is uncurrying )
assume A1: ( f is currying & f is V7() & f is onto ) ; :: thesis: f " is uncurrying
then A2: rng f = the carrier of T by FUNCT_2:def 3;
A3: f " = f " by ;
A4: ( Funcs (X, the carrier of (Z |^ Y)) = the carrier of ((Z |^ Y) |^ X) & Funcs (Y, the carrier of Z) = the carrier of (Z |^ Y) ) by YELLOW_1:28;
hereby :: according to WAYBEL27:def 1 :: thesis: for b1 being set holds
( not b1 in proj1 (f ") or (f ") . b1 = uncurry b1 )
let x be set ; :: thesis: ( x in dom (f ") implies x is Function-yielding Function )
assume x in dom (f ") ; :: thesis:
then x is Element of ((Z |^ Y) |^ X) by YELLOW_0:58;
then x is Function of X,(Funcs (Y, the carrier of Z)) by ;
hence x is Function-yielding Function ; :: thesis: verum
end;
let g be Function; :: thesis: ( not g in proj1 (f ") or (f ") . g = uncurry g )
assume g in dom (f ") ; :: thesis: (f ") . g = uncurry g
then consider h being object such that
A5: h in dom f and
A6: g = f . h by ;
reconsider h = h as Function by A5;
( Funcs ([:X,Y:], the carrier of Z) = the carrier of (Z |^ [:X,Y:]) & h is Element of (Z |^ [:X,Y:]) ) by ;
then h is Function of [:X,Y:], the carrier of Z by FUNCT_2:66;
then A7: dom h = [:X,Y:] by FUNCT_2:def 1;
g = curry h by A1, A5, A6;
then uncurry g = h by ;
hence (f ") . g = uncurry g by ; :: thesis: verum