let p be set ; :: thesis: for A being finite Subset of VAR holds
( p in code A iff ex v1 being Element of VAR st
( v1 in A & p = x". v1 ) )
let A be finite Subset of VAR ; :: thesis: ( p in code A iff ex v1 being Element of VAR st
( v1 in A & p = x". v1 ) )
A1: ( p in code A iff ex q being set st
( q in dom (decode " ) & q in A & p = (decode " ) . q ) ) by FUNCT_1:def 12;
thus ( p in code A implies ex v1 being Element of VAR st
( v1 in A & p = x". v1 ) ) :: thesis: ( ex v1 being Element of VAR st
( v1 in A & p = x". v1 ) implies p in code A )

proof

assume A2: p in code A ; :: thesis: ex v1 being Element of VAR st
( v1 in A & p = x". v1 )
then consider q being set such that
A3: ( q in A & q in dom (decode " ) & p = (decode " ) . q ) by A1;
reconsider p' = p as Element of omega by A2;
reconsider q = q as Element of VAR by A3;
A4: q = decode . p by A3, Lm1, FUNCT_1:57
.= x. (card p') by Def2 ;
take q ; :: thesis: ( q in A & p = x". q )
thus ( q in A & p = x". q ) by A3, A4, Lm2; :: thesis: verum

end;

given v1 being Element of VAR such that A5: ( v1 in A & p = x". v1 ) ; :: thesis: p in code A
p = (decode " ) . v1 by A5, Lm4;
hence p in code A by A5, Lm1, FUNCT_1:def 12; :: thesis: verum