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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:B,A:] or x in rng (Inv (A,B)) )
A1: dom (Inv (A,B)) = [:A,B:] by FUNCT_2:def 1;
assume x in [:B,A:] ; :: thesis: x in rng (Inv (A,B))
then reconsider y = x as Element of [:B,A:] ;
(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)]
.= [(y `1),(y `2)]
.= y by MCART_1:21 ;
hence x in rng (Inv (A,B)) by A1, FUNCT_1:def 3; :: thesis: verum