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 one-to-one & 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 one-to-one & 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 one-to-one & 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 one-to-one & f is onto holds
f " is uncurrying
let f be Function of S,T; :: thesis: ( f is currying & f is one-to-one & f is onto implies f " is uncurrying )
assume A1: ( f is currying & f is one-to-one & f is onto ) ; :: thesis: f " is uncurrying
then ( f " is one-to-one & f " is onto ) by GRCAT_1:56;
then A2: ( rng (f " ) = the carrier of S & rng f = the carrier of T ) by A1, FUNCT_2:def 3;
A3: ( Funcs X,the carrier of (Z |^ Y) = the carrier of ((Z |^ Y) |^ X) & Funcs Y,the carrier of Z = the carrier of (Z |^ Y) & Funcs [:X,Y:],the carrier of Z = the carrier of (Z |^ [:X,Y:]) ) by YELLOW_1:28;

hereby :: according to WAYBEL27:def 1 :: thesis: for b₁ being set holds
( not b₁ in proj1 (f " ) or (f " ) . b₁ = uncurry b₁ )

let x be set ; :: thesis: ( x in dom (f " ) implies x is Function-yielding Function )
assume x in dom (f " ) ; :: thesis: x is Function-yielding Function
then x is Element of ((Z |^ Y) |^ X) by YELLOW_0:59;
then x is Function of X,(Funcs Y,the carrier of Z) by A3, FUNCT_2:121;
hence x is Function-yielding Function ; :: thesis: verum

end;

A4: f " = f " by A1, A2, TOPS_2:def 4;
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 set such that
A5: ( h in dom f & g = f . h ) by A2, FUNCT_1:def 5;
reconsider h = h as Function by A5;
A6: g = curry h by A1, A5, WAYBEL27:def 2;
h is Element of (Z |^ [:X,Y:]) by A5, YELLOW_0:59;
then h is Function of [:X,Y:],the carrier of Z by A3, FUNCT_2:121;
then dom h = [:X,Y:] by FUNCT_2:def 1;
then uncurry g = h by A6, FUNCT_5:56;
hence (f " ) . g = uncurry g by A1, A4, A5, FUNCT_1:54; :: thesis: verum