let p be FinSequence; :: thesis: ProperPrefixes p, dom p are_equipotent
defpred S1[ object , object ] means ex w being FinSequence st
( $1 = w & $2 = (len w) + 1 );
A1: for x being object st x in ProperPrefixes p holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in ProperPrefixes p implies ex y being object st S1[x,y] )
assume x in ProperPrefixes p ; :: thesis: ex y being object st S1[x,y]
then consider q being FinSequence such that
A2: x = q and
q is_a_proper_prefix_of p by Def2;
reconsider y = (len q) + 1 as set ;
take y ; :: thesis: S1[x,y]
take q ; :: thesis: ( x = q & y = (len q) + 1 )
thus ( x = q & y = (len q) + 1 ) by A2; :: thesis: verum
end;
consider f being Function such that
A3: dom f = ProperPrefixes p and
A4: for x being object st x in ProperPrefixes p holds
S1[x,f . x] from CLASSES1:sch 1(A1);
 take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = ProperPrefixes p & rng f = dom p )
thus f is one-to-one :: thesis: ( dom f = ProperPrefixes p & rng f = dom p )
proof
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A5: ( x in dom f & y in dom f ) and
A6: 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 A3, A4, A5, A6;
hence x = y by A3, A5, Th3, Th17; :: thesis: verum
end;
thus dom f = ProperPrefixes p by A3; :: thesis: rng f = dom p
thus rng f c= dom p :: according to XBOOLE_0:def 10 :: thesis: dom p is_a_prefix_of rng f
proof
let x be object ; :: 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 object such that
A7: y in dom f and
A8: x = f . y by FUNCT_1:def 3;
consider q being FinSequence such that
A9: y = q and
A10: x = (len q) + 1 by A3, A4, A7, A8;
len q < len p by A3, A7, A9, Th12;
then ( 0 + 1 <= (len q) + 1 & (len q) + 1 <= len p ) by NAT_1:13;
then x in Seg (len p) by A10, FINSEQ_1:1;
hence x in dom p by FINSEQ_1:def 3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom p or x in rng f )
assume A11: x in dom p ; :: thesis: x in rng f
then A12: x in Seg (len p) by FINSEQ_1:def 3;
reconsider n = x as Nat by A11;
A13: 1 <= n by A12, FINSEQ_1:1;
A14: n <= len p by A12, FINSEQ_1:1;
consider m being Nat such that
A15: n = 1 + m by A13, NAT_1:10;
reconsider m = m as Nat ;
reconsider q = p | (Seg m) as FinSequence by FINSEQ_1:15;
A16: m <= len p by A14, A15, NAT_1:13;
A17: m <> len p by A14, A15, NAT_1:13;
A18: len q = m by A16, FINSEQ_1:17;
A19: q is_a_prefix_of p ;
len q = m by A16, FINSEQ_1:17;
then q is_a_proper_prefix_of p by A17, A19;
then A20: q in ProperPrefixes p by Th11;
then ex r being FinSequence st
( q = r & f . q = (len r) + 1 ) by A4;
hence x in rng f by A3, A15, A18, A20, FUNCT_1:def 3; :: thesis: verum