let k be Element of NAT ; :: thesis: ( k = len p iff Seg k = dom p )
consider n being Nat such that
A1: dom p = Seg n by Def2;
dom p,p are_equipotent

proof

deffunc H₁( object ) -> object = [$1,(p . $1)];
consider g being Function such that
A2: dom g = dom p and
A3: for x being object st x in dom p holds
g . x = H₁(x) from FUNCT_1:sch 3();
take g ; :: according to WELLORD2:def 4 :: thesis: ( g is one-to-one & dom g = dom p & rng g = p )
thus g is one-to-one :: thesis: ( dom g = dom p & rng g = p )

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
assume that
A4: x in dom g and
A5: y in dom g ; :: thesis: ( not g . x = g . y or x = y )
assume g . x = g . y ; :: thesis: x = y
then [x,(p . x)] = g . y by A2, A3, A4
.= [y,(p . y)] by A2, A3, A5 ;
hence x = y by XTUPLE_0:1; :: thesis: verum

end;

thus dom g = dom p by A2; :: thesis: rng g = p
thus rng g c= p :: according to XBOOLE_0:def 10 :: thesis: p c= rng g

proof

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in rng g or i in p )
assume i in rng g ; :: thesis: i in p
then consider x being object such that
A6: x in dom g and
A7: g . x = i by FUNCT_1:def 3;
g . x = [x,(p . x)] by A2, A3, A6;
hence i in p by A2, A6, A7, FUNCT_1:1; :: thesis: verum

end;

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in p or [x,y] in rng g )
assume A8: [x,y] in p ; :: thesis: [x,y] in rng g
then A9: x in dom p by FUNCT_1:1;
y = p . x by A8, FUNCT_1:1;
then g . x = [x,y] by A3, A8, FUNCT_1:1;
hence [x,y] in rng g by A2, A9, FUNCT_1:def 3; :: thesis: verum

end;

then A10: card p = card (dom p) by CARD_1:5;
thus ( k = card p implies Seg k = dom p ) by A1, A10, Lm1, CARD_1:def 2; :: thesis: ( Seg k = dom p implies k = len p )
assume Seg k = dom p ; :: thesis: k = len p
hence k = card p by A10, Lm1, CARD_1:def 2; :: thesis: verum