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₁( set ) -> set = [$1,(p . $1)];
consider g being Function such that
A2: dom g = dom p and
A3: for x being set 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 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in dom g or not b₁ in dom g or not g . x = g . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in dom g or not y in dom g or not g . x = g . y or x = y )
assume A4: ( x in dom g & 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, A4 ;
hence x = y by ZFMISC_1:33; :: 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 set ; :: 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 set such that
A5: x in dom g and
A6: g . x = i by FUNCT_1:def 5;
g . x = [x,(p . x)] by A2, A3, A5;
hence i in p by A2, A5, A6, FUNCT_1:8; :: thesis: verum

end;

let x, y be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in p or [x,y] in rng g )
assume [x,y] in p ; :: thesis: [x,y] in rng g
then A7: ( x in dom p & y = p . x ) by FUNCT_1:8;
then g . x = [x,y] by A3;
hence [x,y] in rng g by A2, A7, FUNCT_1:def 5; :: thesis: verum

end;

then A8: card p = card (dom p) by CARD_1:21;
thus ( k = card p implies Seg k = dom p ) :: thesis: ( Seg k = dom p implies k = len p )

proof

assume k = card p ; :: thesis: Seg k = dom p
then k = card n by A1, A8, Lm2;
hence Seg k = dom p by A1, CARD_1:def 5; :: thesis: verum

end;

assume A9: Seg k = dom p ; :: thesis: k = len p
thus k = card k by CARD_1:def 5
.= card p by A8, A9, Lm2 ; :: thesis: verum