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 T,S st f is uncurrying & f is V7() & f is onto holds

f " is currying

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 T,S st f is uncurrying & f is V7() & f is onto holds

f " is currying

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 T,S st f is uncurrying & f is V7() & f is onto holds

f " is currying

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

f " is currying

let f be Function of T,S; :: thesis: ( f is uncurrying & f is V7() & f is onto implies f " is currying )

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

assume A2: ( f is uncurrying & f is V7() & f is onto ) ; :: thesis: f " is currying

then A3: rng f = the carrier of S by FUNCT_2:def 3;

A4: f " = f " by A2, TOPS_2:def 4;

A5: Funcs ([:X,Y:], the carrier of Z) = the carrier of (Z |^ [:X,Y:]) by YELLOW_1:28;

assume g in dom (f ") ; :: thesis: (f ") . g = curry g

then consider h being object such that

A6: h in dom f and

A7: g = f . h by A3, FUNCT_1:def 3;

reconsider h = h as Function by A6;

h is Element of ((Z |^ Y) |^ X) by A6, YELLOW_0:58;

then h is Function of X,(Funcs (Y, the carrier of Z)) by A1, FUNCT_2:66;

then A8: rng h c= Funcs (Y, the carrier of Z) by RELAT_1:def 19;

g = uncurry h by A2, A6, A7;

then curry g = h by A8, FUNCT_5:48;

hence (f ") . g = curry g by A2, A4, A6, A7, FUNCT_1:32; :: thesis: verum

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 T,S st f is uncurrying & f is V7() & f is onto holds

f " is currying

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 T,S st f is uncurrying & f is V7() & f is onto holds

f " is currying

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 T,S st f is uncurrying & f is V7() & f is onto holds

f " is currying

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

f " is currying

let f be Function of T,S; :: thesis: ( f is uncurrying & f is V7() & f is onto implies f " is currying )

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

assume A2: ( f is uncurrying & f is V7() & f is onto ) ; :: thesis: f " is currying

then A3: rng f = the carrier of S by FUNCT_2:def 3;

A4: f " = f " by A2, TOPS_2:def 4;

A5: Funcs ([:X,Y:], the carrier of Z) = the carrier of (Z |^ [:X,Y:]) by YELLOW_1:28;

hereby :: according to WAYBEL27:def 2 :: thesis: for b_{1} being set holds

( not b_{1} in proj1 (f ") or (f ") . b_{1} = curry b_{1} )

let g be Function; :: thesis: ( not g in proj1 (f ") or (f ") . g = curry g )( not b

let x be set ; :: thesis: ( x in dom (f ") implies ( x is Function & proj1 x is Relation ) )

assume x in dom (f ") ; :: thesis: ( x is Function & proj1 x is Relation )

then x is Element of (Z |^ [:X,Y:]) by YELLOW_0:58;

then reconsider g = x as Function of [:X,Y:], the carrier of Z by A5, FUNCT_2:66;

dom g = proj1 g ;

hence ( x is Function & proj1 x is Relation ) ; :: thesis: verum

end;assume x in dom (f ") ; :: thesis: ( x is Function & proj1 x is Relation )

then x is Element of (Z |^ [:X,Y:]) by YELLOW_0:58;

then reconsider g = x as Function of [:X,Y:], the carrier of Z by A5, FUNCT_2:66;

dom g = proj1 g ;

hence ( x is Function & proj1 x is Relation ) ; :: thesis: verum

assume g in dom (f ") ; :: thesis: (f ") . g = curry g

then consider h being object such that

A6: h in dom f and

A7: g = f . h by A3, FUNCT_1:def 3;

reconsider h = h as Function by A6;

h is Element of ((Z |^ Y) |^ X) by A6, YELLOW_0:58;

then h is Function of X,(Funcs (Y, the carrier of Z)) by A1, FUNCT_2:66;

then A8: rng h c= Funcs (Y, the carrier of Z) by RELAT_1:def 19;

g = uncurry h by A2, A6, A7;

then curry g = h by A8, FUNCT_5:48;

hence (f ") . g = curry g by A2, A4, A6, A7, FUNCT_1:32; :: thesis: verum