let X, Y be non empty set ; 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 ; 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:]; 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; 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; ( f is currying & f is V7() & f is onto implies f " is uncurrying )
assume A1:
( f is currying & f is V7() & f is onto )
; f " is uncurrying
then A2:
rng f = the carrier of T
by FUNCT_2:def 3;
A3:
f " = f "
by A1, TOPS_2:def 4;
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;
let g be Function; ( not g in proj1 (f ") or (f ") . g = uncurry g )
assume
g in dom (f ")
; (f ") . g = uncurry g
then consider h being object such that
A5:
h in dom f
and
A6:
g = f . h
by A2, FUNCT_1:def 3;
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 A5, YELLOW_0:58, YELLOW_1:28;
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 A7, FUNCT_5:49;
hence
(f ") . g = uncurry g
by A1, A3, A5, A6, FUNCT_1:32; verum