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 & proj1 g = dom p & proj2 g = p )
thus g is one-to-one :: thesis: ( proj1 g = dom p & proj2 g = p )

proof

let x be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x in proj1 g or not b₁ in proj1 g or not g . x = g . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 g or not y in proj1 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 ZFMISC_1:27; :: thesis: verum

end;

thus dom g = dom p by A2; :: thesis: proj2 g = p
thus rng g c= p :: according to XBOOLE_0:def 10 :: thesis: p c= proj2 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
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 set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in p or [x,y] in proj2 g )
assume A8: [x,y] in p ; :: thesis: [x,y] in proj2 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, A9;
hence [x,y] in proj2 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 ) :: 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, A10, Lm2;
hence Seg k = dom p by A1, CARD_1:def 2; :: thesis: verum

end;

assume A11: Seg k = dom p ; :: thesis: k = len p
thus k = card k by CARD_1:def 2
.= card p by A10, A11, Lm2 ; :: thesis: verum