let X, Y, Z be non empty set ; :: thesis: for f being Function of X,[:Y,Z:]

for x being Element of X holds (f ~) . x = [((f . x) `2),((f . x) `1)]

let f be Function of X,[:Y,Z:]; :: thesis: for x being Element of X holds (f ~) . x = [((f . x) `2),((f . x) `1)]

let x be Element of X; :: thesis: (f ~) . x = [((f . x) `2),((f . x) `1)]

x in X ;

then A1: x in dom f by FUNCT_2:def 1;

f . x = [((f . x) `1),((f . x) `2)] by MCART_1:22;

hence (f ~) . x = [((f . x) `2),((f . x) `1)] by A1, Def1; :: thesis: verum

for x being Element of X holds (f ~) . x = [((f . x) `2),((f . x) `1)]

let f be Function of X,[:Y,Z:]; :: thesis: for x being Element of X holds (f ~) . x = [((f . x) `2),((f . x) `1)]

let x be Element of X; :: thesis: (f ~) . x = [((f . x) `2),((f . x) `1)]

x in X ;

then A1: x in dom f by FUNCT_2:def 1;

f . x = [((f . x) `1),((f . x) `2)] by MCART_1:22;

hence (f ~) . x = [((f . x) `2),((f . x) `1)] by A1, Def1; :: thesis: verum