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