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:24;
hence (f ~ ) . x = [((f . x) `2 ),((f . x) `1 )] by A1, Def1; :: thesis: verum