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 object st
( q in dom (decode ") & q in A & p = (decode ") . q ) ) by FUNCT_1:def 6;
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 reconsider p9 = p as Element of omega ;
consider q being set such that
A3: q in A and
q in dom (decode ") and
A4: p = (decode ") . q by A1, A2;
reconsider q = q as Element of VAR by A3;
take q ; :: thesis: ( q in A & p = x". q )
q = decode . p by A4, Lm1, FUNCT_1:35
.= x. (card p9) by Def1 ;
hence ( q in A & p = x". q ) by A3, Lm2; :: thesis: verum
end;
given v1 being Element of VAR such that A5: v1 in A and
A6: p = x". v1 ; :: thesis: p in code A
p = (decode ") . v1 by A6, Lm4;
hence p in code A by A5, Lm1, FUNCT_1:def 6; :: thesis: verum