let X, Y, Z be non empty set ; 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:]; for x being Element of X holds (f ~) . x = [((f . x) `2),((f . x) `1)]
let x be Element of X; (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; verum