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

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

now

assume p in VAR ; :: thesis: ex q being Element of NAT st
( q in dom decode & decode . q = p )
then reconsider p9 = p as Element of VAR ;
take q = x". p9; :: 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 Def2
.= x. (x". p9) by CARD_1:def 5
.= p by Def3 ; :: thesis: verum

end;

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

end;

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

now

let p, q be set ; :: 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, Def2
.= x. (card q9) by Def2 ;
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_1:def 5
.= card k1 by A5, A7, XCMPLX_1:2
.= k1 by CARD_1:def 5 ;
hence p = q by A6, A7; :: thesis: verum

end;

hence A8: decode is one-to-one by FUNCT_1:def 8; :: 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:55; :: thesis: verum