thus A1: dom decode = omega by FUNCT_2:def 1; :: thesis: ( rng decode = VAR & decode is one-to-one & decode " is one-to-one & dom (decode ") = VAR & rng (decode ") = omega )

now :: thesis: for p being object holds
( p in VAR iff ex q being object st
( q in dom decode & p = decode . q ) )

let p be object ; :: thesis: ( p in VAR iff ex q being object st
( q in dom decode & p = decode . q ) )

now :: thesis: ( p in VAR implies ex q being object st
( q in dom decode & decode . q = p ) )

assume p in VAR ; :: thesis: ex q being object st
( q in dom decode & decode . q = p )
then reconsider p9 = p as Element of VAR ;
reconsider q = x". p9 as object ;
take q = q; :: thesis: ( q in dom decode & decode . q = p )
thus q in dom decode by A1; :: thesis: decode . q = p
thus decode . q = x. (card (x". p9)) by Def1
.= x. (x". p9)
.= p by Def2 ; :: thesis: verum

end;

hence ( p in VAR iff ex q being object st
( q in dom decode & p = decode . q ) ) by FUNCT_2:5; :: thesis: verum

end;

hence A2: rng decode = VAR by FUNCT_1:def 3; :: thesis: ( decode is one-to-one & decode " is one-to-one & dom (decode ") = VAR & rng (decode ") = omega )

now :: thesis: for p, q being object st p in dom decode & q in dom decode & decode . p = decode . q holds
p = q

let p, q be object ; :: thesis: ( p in dom decode & q in dom decode & decode . p = decode . q implies p = q )
assume that
A3: ( p in dom decode & q in dom decode ) and
A4: decode . p = decode . q ; :: thesis: p = q
reconsider p9 = p, q9 = q as Element of omega by A3;
x. (card p9) = decode . q by A4, Def1
.= x. (card q9) by Def1 ;
then A5: 5 + (card p9) = x. (card q9) by ZF_LANG:def 2
.= 5 + (card q9) by ZF_LANG:def 2 ;
consider k being Element of NAT such that
A6: p9 = k ;
consider k1 being Element of NAT such that
A7: q9 = k1 ;
k = card p9 by A6
.= card k1 by A5, A7, XCMPLX_1:2
.= k1 ;
hence p = q by A6, A7; :: thesis: verum

end;

hence A8: decode is one-to-one by FUNCT_1:def 4; :: thesis: ( decode " is one-to-one & dom (decode ") = VAR & rng (decode ") = omega )
hence decode " is one-to-one ; :: thesis: ( dom (decode ") = VAR & rng (decode ") = omega )
thus ( dom (decode ") = VAR & rng (decode ") = omega ) by A1, A2, A8, FUNCT_1:33; :: thesis: verum