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 )
thus A2: rng decode = VAR :: thesis: ( decode is one-to-one & decode " is one-to-one & dom (decode " ) = VAR & rng (decode " ) = omega )

proof

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 p' = p as Element of VAR ;
take q = x". p'; :: 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". p')) by Def2
.= x. (x". p') 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 rng decode = VAR by FUNCT_1:def 5; :: thesis: verum

end;

thus A3: decode is one-to-one :: thesis: ( decode " is one-to-one & dom (decode " ) = VAR & rng (decode " ) = omega )

proof

now

let p, q be set ; :: thesis: ( p in dom decode & q in dom decode & decode . p = decode . q implies p = q )
assume A4: ( p in dom decode & q in dom decode & decode . p = decode . q ) ; :: thesis: p = q
then reconsider p' = p, q' = q as Element of omega ;
x. (card p') = decode . q by A4, Def2
.= x. (card q') by Def2 ;
then A5: 5 + (card p') = x. (card q') by ZF_LANG:def 2
.= 5 + (card q') by ZF_LANG:def 2 ;
consider k being Element of NAT such that
A6: p' = k ;
consider k1 being Element of NAT such that
A7: q' = k1 ;
k = card p' 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 decode is one-to-one by FUNCT_1:def 8; :: thesis: verum

end;

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