let A, B be non empty set ; :: thesis: rng (Inv A,B) = [:B,A:]
thus rng (Inv A,B) c= [:B,A:] ; :: according to XBOOLE_0:def 10 :: thesis: [:B,A:] c= rng (Inv A,B)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:B,A:] or x in rng (Inv A,B) )
assume x in [:B,A:] ; :: thesis: x in rng (Inv A,B)
then reconsider y = x as Element of [:B,A:] ;
A1: ( [(y `2 ),(y `1 )] in [:A,B:] & dom (Inv A,B) = [:A,B:] ) by FUNCT_2:def 1;
(Inv A,B) . [(y `2 ),(y `1 )] = [([(y `2 ),(y `1 )] `2 ),([(y `2 ),(y `1 )] `1 )] by Def6
.= [(y `1 ),([(y `2 ),(y `1 )] `1 )] by MCART_1:7
.= [(y `1 ),(y `2 )] by MCART_1:7
.= y by MCART_1:23 ;
hence x in rng (Inv A,B) by A1, FUNCT_1:def 5; :: thesis: verum