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

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