let p be FinSequence; :: thesis: ProperPrefixes p, dom p are_equipotent
defpred S₁[ set , set ] means ex w being FinSequence st
( $1 = w & $2 = (len w) + 1 );
A1: for x being set st x in ProperPrefixes p holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in ProperPrefixes p implies ex y being set st S₁[x,y] )
assume x in ProperPrefixes p ; :: thesis: ex y being set st S₁[x,y]
then consider q being FinSequence such that
A3: x = q and
q is_a_proper_prefix_of p by Def4;
reconsider y = (len q) + 1 as set ;
take y ; :: thesis: S₁[x,y]
take q ; :: thesis: ( x = q & y = (len q) + 1 )
thus ( x = q & y = (len q) + 1 ) by A3; :: thesis: verum

end;

consider f being Function such that
A4: dom f = ProperPrefixes p and
A5: for x being set st x in ProperPrefixes p holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = ProperPrefixes p & proj2 f = dom p )
thus f is one-to-one :: thesis: ( proj1 f = ProperPrefixes p & proj2 f = dom p )

proof

let x be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x in proj1 f or not b₁ in proj1 f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A6: ( x in dom f & y in dom f ) and
A7: f . x = f . y ; :: thesis: x = y
( ex q being FinSequence st
( x = q & f . x = (len q) + 1 ) & ex r being FinSequence st
( y = r & f . x = (len r) + 1 ) ) by A4, A5, A6, A7;
hence x = y by A4, A6, Th19, Th42; :: thesis: verum

end;

thus dom f = ProperPrefixes p by A4; :: thesis: proj2 f = dom p
thus rng f c= dom p :: according to XBOOLE_0:def 10 :: thesis: dom p is_a_prefix_of proj2 f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in dom p )
assume x in rng f ; :: thesis: x in dom p
then consider y being set such that
A10: y in dom f and
A11: x = f . y by FUNCT_1:def 5;
consider q being FinSequence such that
A12: y = q and
A13: x = (len q) + 1 by A4, A5, A10, A11;
len q < len p by A4, A10, A12, Th37;
then ( 0 + 1 <= (len q) + 1 & (len q) + 1 <= len p ) by NAT_1:13;
then x in Seg (len p) by A13, FINSEQ_1:3;
hence x in dom p by FINSEQ_1:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom p or x in proj2 f )
assume A17: x in dom p ; :: thesis: x in proj2 f
then A18: x in Seg (len p) by FINSEQ_1:def 3;
reconsider n = x as Element of NAT by A17;
A19: 1 <= n by A18, FINSEQ_1:3;
A20: n <= len p by A18, FINSEQ_1:3;
consider m being Nat such that
A21: n = 1 + m by A19, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
reconsider q = p | (Seg m) as FinSequence by FINSEQ_1:19;
A22: m <= len p by A20, A21, NAT_1:13;
A23: m <> len p by A20, A21, NAT_1:13;
A24: len q = m by A22, FINSEQ_1:21;
A25: q is_a_prefix_of p by Def1;
len q = m by A22, FINSEQ_1:21;
then q is_a_proper_prefix_of p by A23, A25, XBOOLE_0:def 8;
then A28: q in ProperPrefixes p by Th36;
then ex r being FinSequence st
( q = r & f . q = (len r) + 1 ) by A5;
hence x in proj2 f by A4, A21, A24, A28, FUNCT_1:def 5; :: thesis: verum