defpred S1[ Nat, set , set ] means P1[\$1,\$2,\$3];
A2: for x being Element of NAT
for y being Element of F1() ex z being Element of F1() st S1[x,y,z] by A1;
consider f being Function of [:NAT,F1():],F1() such that
A3: for x being Element of NAT
for y being Element of F1() holds S1[x,y,f . (x,y)] from defpred S2[ FinSequence] means ( \$1 . 1 = F2() & ( for n being Nat st n + 2 <= len \$1 holds
\$1 . (n + 2) = f . [n,(\$1 . (n + 1))] ) );
consider X being set such that
A4: for x being object holds
( x in X iff ex p being FinSequence st
( p in F1() * & S2[p] & x = p ) ) from set Y = union X;
A5: for x being set st x in X holds
x in F1() *
proof
let x be set ; :: thesis: ( x in X implies x in F1() * )
assume x in X ; :: thesis: x in F1() *
then ex p being FinSequence st
( p in F1() * & p . 1 = F2() & ( for n being Nat st n + 2 <= len p holds
p . (n + 2) = f . [n,(p . (n + 1))] ) & x = p ) by A4;
hence x in F1() * ; :: thesis: verum
end;
A6: for p, q being FinSequence st p in X & q in X & len p <= len q holds
p c= q
proof
let p, q be FinSequence; :: thesis: ( p in X & q in X & len p <= len q implies p c= q )
assume that
A7: p in X and
A8: q in X and
A9: len p <= len q ; :: thesis: p c= q
A10: ex q9 being FinSequence st
( q9 in F1() * & q9 . 1 = F2() & ( for n being Nat st n + 2 <= len q9 holds
q9 . (n + 2) = f . [n,(q9 . (n + 1))] ) & q = q9 ) by A4, A8;
A11: ex p9 being FinSequence st
( p9 in F1() * & p9 . 1 = F2() & ( for n being Nat st n + 2 <= len p9 holds
p9 . (n + 2) = f . [n,(p9 . (n + 1))] ) & p = p9 ) by A4, A7;
A12: for n being Nat st 1 <= n & n <= len p holds
p . n = q . n
proof
defpred S3[ Nat] means ( 1 <= \$1 & \$1 <= len p & p . \$1 <> q . \$1 );
assume ex n being Nat st S3[n] ; :: thesis: contradiction
then A13: ex n being Nat st S3[n] ;
consider k being Nat such that
A14: ( S3[k] & ( for n being Nat st S3[n] holds
k <= n ) ) from k = 1
proof
0 <> k by A14;
then consider n being Nat such that
A15: k = n + 1 by NAT_1:6;
n + 0 <= n + 1 by XREAL_1:7;
then A16: n <= len p by ;
A17: n + 0 < n + 1 by XREAL_1:6;
assume A18: k <> 1 ; :: thesis: contradiction
then 1 < n + 1 by ;
then A19: 1 <= n by NAT_1:13;
n <> 0 by ;
then consider m being Nat such that
A20: n = m + 1 by NAT_1:6;
reconsider m = m as Nat ;
A21: m + 2 <= len q by ;
p . k = p . (m + (1 + 1)) by
.= f . [m,(p . n)] by A11, A14, A15, A20
.= f . [m,(q . (m + 1))] by A14, A15, A19, A16, A17, A20
.= q . k by A10, A15, A20, A21 ;
hence contradiction by A14; :: thesis: verum
end;
hence contradiction by A11, A10, A14; :: thesis: verum
end;
now :: thesis: for x being object st x in p holds
x in q
let x be object ; :: thesis: ( x in p implies x in q )
assume x in p ; :: thesis: x in q
then consider n being Nat such that
A22: n in dom p and
A23: x = [n,(p . n)] by FINSEQ_1:12;
A24: n in Seg (len p) by ;
then A25: 1 <= n by FINSEQ_1:1;
A26: n <= len p by ;
then n <= len q by ;
then n in Seg (len q) by ;
then A27: n in dom q by FINSEQ_1:def 3;
x = [n,(q . n)] by A12, A23, A25, A26;
hence x in q by ; :: thesis: verum
end;
hence p c= q ; :: thesis: verum
end;
A28: union X is Function-like
proof
let x, y, z be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y] in union X or not [x,z] in union X or y = z )
assume that
A29: [x,y] in union X and
A30: [x,z] in union X ; :: thesis: y = z
consider Z2 being set such that
A31: [x,z] in Z2 and
A32: Z2 in X by ;
Z2 in F1() * by ;
then reconsider q = Z2 as FinSequence of F1() by FINSEQ_1:def 11;
consider Z1 being set such that
A33: [x,y] in Z1 and
A34: Z1 in X by ;
Z1 in F1() * by ;
then reconsider p = Z1 as FinSequence of F1() by FINSEQ_1:def 11;
per cases ( len q <= len p or len p <= len q ) ;
suppose len q <= len p ; :: thesis: y = z
then A35: q c= Z1 by A6, A34, A32;
[x,y] in p by A33;
hence y = z by ; :: thesis: verum
end;
suppose len p <= len q ; :: thesis: y = z
then p c= Z2 by A6, A34, A32;
then [x,y] in q by A33;
hence y = z by ; :: thesis: verum
end;
end;
end;
union X is Relation-like
proof
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in union X or ex b1, b2 being object st x = [b1,b2] )
assume x in union X ; :: thesis: ex b1, b2 being object st x = [b1,b2]
then consider Z2 being set such that
A36: x in Z2 and
A37: Z2 in X by TARSKI:def 4;
ex p being FinSequence st
( p in F1() * & S2[p] & Z2 = p ) by ;
then Z2 is Relation-like ;
hence ex y, z being object st x = [y,z] by A36; :: thesis: verum
end;
then consider g being Function such that
A38: g = union X by A28;
A39: for x being object st x in rng g holds
x in F1()
proof
let x be object ; :: thesis: ( x in rng g implies x in F1() )
assume x in rng g ; :: thesis: x in F1()
then consider y being object such that
A40: ( y in dom g & x = g . y ) by FUNCT_1:def 3;
[y,x] in union X by ;
then consider Z being set such that
A41: [y,x] in Z and
A42: Z in X by TARSKI:def 4;
Z in F1() * by ;
then reconsider p = Z as FinSequence of F1() by FINSEQ_1:def 11;
( y in dom p & x = p . y ) by ;
then A43: x in rng p by FUNCT_1:def 3;
rng p c= F1() by FINSEQ_1:def 4;
hence x in F1() by A43; :: thesis: verum
end;
then rng g c= F1() ;
then reconsider h = g as Function of (dom g),F1() by FUNCT_2:2;
A44: for n being Nat holds n + 1 in dom h
proof
defpred S3[ Nat] means \$1 + 1 in dom h;
A45: for n being Nat st n + 2 <= len <*F2()*> holds
<*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))]
proof
let n be Nat; :: thesis: ( n + 2 <= len <*F2()*> implies <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] )
assume n + 2 <= len <*F2()*> ; :: thesis: <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))]
then n + 2 <= 1 by FINSEQ_1:39;
then n + (1 + 1) <= n + 1 by NAT_1:12;
hence <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] by XREAL_1:6; :: thesis: verum
end;
( <*F2()*> . 1 = F2() & <*F2()*> in F1() * ) by ;
then <*F2()*> in X by ;
then A46: {[1,F2()]} in X by FINSEQ_1:37;
A47: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume k + 1 in dom h ; :: thesis: S3[k + 1]
then [(k + 1),(h . (k + 1))] in union X by ;
then consider Z being set such that
A48: [(k + 1),(h . (k + 1))] in Z and
A49: Z in X by TARSKI:def 4;
Z in F1() * by ;
then reconsider Z = Z as FinSequence of F1() by FINSEQ_1:def 11;
A50: ( k + 1 = len Z implies S3[k + 1] )
proof
set p = Z ^ <*(f . [k,(Z . (k + 1))])*>;
A51: 1 <= (k + 1) + 1 by NAT_1:12;
assume A52: k + 1 = len Z ; :: thesis: S3[k + 1]
then 1 <= len Z by NAT_1:12;
then 1 in Seg (len Z) by FINSEQ_1:1;
then A53: 1 in dom Z by FINSEQ_1:def 3;
A54: for n being Nat st n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) holds
(Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]
proof
let n be Nat; :: thesis: ( n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] )
assume n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) ; :: thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]
then A55: n + 2 <= (len Z) + (len <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:22;
then A56: n + 2 <= (len Z) + 1 by FINSEQ_1:40;
A57: ( n + 2 <> (len Z) + 1 implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] )
proof
(n + 1) + 1 <= (len Z) + 1 by ;
then ( 1 <= n + 1 & n + 1 <= len Z ) by ;
then n + 1 in Seg (len Z) by FINSEQ_1:1;
then A58: n + 1 in dom Z by FINSEQ_1:def 3;
A59: 1 <= n + (1 + 1) by NAT_1:12;
assume A60: n + 2 <> (len Z) + 1 ; :: thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]
then n + 2 <= len Z by ;
then n + 2 in Seg (len Z) by ;
then A61: n + 2 in dom Z by FINSEQ_1:def 3;
ex q being FinSequence st
( q in F1() * & q . 1 = F2() & ( for n being Nat st n + 2 <= len q holds
q . (n + 2) = f . [n,(q . (n + 1))] ) & Z = q ) by ;
then Z . (n + 2) = f . [n,(Z . (n + 1))] by ;
then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,(Z . (n + 1))] by ;
hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by ; :: thesis: verum
end;
( n + 2 = (len Z) + 1 implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] )
proof
(n + 1) + 1 <= (len Z) + 1 by ;
then ( 1 <= n + 1 & n + 1 <= len Z ) by ;
then n + 1 in Seg (len Z) by FINSEQ_1:1;
then A62: n + 1 in dom Z by FINSEQ_1:def 3;
assume A63: n + 2 = (len Z) + 1 ; :: thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]
then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = <*(f . [k,(Z . (k + 1))])*> . ((n + 2) - ((n + 2) - 1)) by
.= f . [n,(Z . (n + 1))] by ;
hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by ; :: thesis: verum
end;
hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A57; :: thesis: verum
end;
A64: Z ^ <*(f . [k,(Z . (k + 1))])*> in F1() *
proof
1 <= k + 1 by NAT_1:12;
then k + 1 in Seg (len Z) by ;
then k + 1 in dom Z by FINSEQ_1:def 3;
then A65: Z . (k + 1) in rng Z by FUNCT_1:def 3;
rng Z c= F1() by FINSEQ_1:def 4;
then reconsider z = Z . (k + 1) as Element of F1() by A65;
reconsider n = k as Element of NAT by ORDINAL1:def 12;
Z ^ <*(f . [k,(Z . (k + 1))])*> = Z ^ <*(f . [n,z])*> ;
hence Z ^ <*(f . [k,(Z . (k + 1))])*> in F1() * by FINSEQ_1:def 11; :: thesis: verum
end;
len (Z ^ <*(f . [k,(Z . (k + 1))])*>) = (len Z) + (len <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:22
.= (k + 1) + 1 by ;
then (k + 1) + 1 in Seg (len (Z ^ <*(f . [k,(Z . (k + 1))])*>)) by ;
then (k + 1) + 1 in dom (Z ^ <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:def 3;
then A66: [((k + 1) + 1),((Z ^ <*(f . [k,(Z . (k + 1))])*>) . ((k + 1) + 1))] in Z ^ <*(f . [k,(Z . (k + 1))])*> by FUNCT_1:1;
ex p being FinSequence st
( p in F1() * & p . 1 = F2() & ( for n being Nat st n + 2 <= len p holds
p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by ;
then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . 1 = F2() by ;
then Z ^ <*(f . [k,(Z . (k + 1))])*> in X by A4, A64, A54;
then [((k + 1) + 1),((Z ^ <*(f . [k,(Z . (k + 1))])*>) . ((k + 1) + 1))] in h by ;
hence S3[k + 1] by FUNCT_1:1; :: thesis: verum
end;
( k + 1 <> len Z implies S3[k + 1] )
proof
k + 1 in dom Z by ;
then k + 1 in Seg (len Z) by FINSEQ_1:def 3;
then A67: k + 1 <= len Z by FINSEQ_1:1;
assume k + 1 <> len Z ; :: thesis: S3[k + 1]
then k + 1 < len Z by ;
then A68: (k + 1) + 1 <= len Z by NAT_1:13;
1 <= (k + 1) + 1 by NAT_1:12;
then (k + 1) + 1 in Seg (len Z) by ;
then (k + 1) + 1 in dom Z by FINSEQ_1:def 3;
then [((k + 1) + 1),(Z . ((k + 1) + 1))] in Z by FUNCT_1:1;
then [((k + 1) + 1),(Z . ((k + 1) + 1))] in h by ;
hence S3[k + 1] by FUNCT_1:1; :: thesis: verum
end;
hence S3[k + 1] by A50; :: thesis: verum
end;
[1,F2()] in {[1,F2()]} by TARSKI:def 1;
then [1,F2()] in h by ;
then A69: S3[ 0 ] by FUNCT_1:1;
thus for k being Nat holds S3[k] from :: thesis: verum
end;
A70: for n being Nat holds h . (n + 2) = f . [n,(h . (n + 1))]
proof
let n be Nat; :: thesis: h . (n + 2) = f . [n,(h . (n + 1))]
(n + 1) + 1 in dom h by A44;
then [(n + 2),(h . (n + 2))] in h by FUNCT_1:def 2;
then consider Z being set such that
A71: [(n + 2),(h . (n + 2))] in Z and
A72: Z in X by ;
A73: ex p being FinSequence st
( p in F1() * & p . 1 = F2() & ( for n being Nat st n + 2 <= len p holds
p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by ;
Z in F1() * by ;
then reconsider Z = Z as FinSequence of F1() by FINSEQ_1:def 11;
n + 2 in dom Z by ;
then n + 2 in Seg (len Z) by FINSEQ_1:def 3;
then A74: n + 2 <= len Z by FINSEQ_1:1;
n + 1 <= n + 2 by XREAL_1:7;
then ( 1 <= n + 1 & n + 1 <= len Z ) by ;
then n + 1 in Seg (len Z) by FINSEQ_1:1;
then n + 1 in dom Z by FINSEQ_1:def 3;
then [(n + 1),(Z . (n + 1))] in Z by FUNCT_1:1;
then A75: [(n + 1),(Z . (n + 1))] in h by ;
thus h . (n + 2) = Z . (n + 2) by
.= f . [n,(Z . (n + 1))] by
.= f . [n,(h . (n + 1))] by ; :: thesis: verum
end;
defpred S3[ object , object ] means ex n being Nat st
( n = \$1 & \$2 = h . (n + 1) );
A76: for x being object st x in NAT holds
ex y being object st S3[x,y]
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st S3[x,y] )
assume x in NAT ; :: thesis: ex y being object st S3[x,y]
then reconsider n = x as Nat ;
take h . (n + 1) ; :: thesis: S3[x,h . (n + 1)]
take n ; :: thesis: ( n = x & h . (n + 1) = h . (n + 1) )
thus ( n = x & h . (n + 1) = h . (n + 1) ) ; :: thesis: verum
end;
consider g being Function such that
A77: ( dom g = NAT & ( for x being object st x in NAT holds
S3[x,g . x] ) ) from A78: dom g = NAT by A77;
A79: for n being Nat holds g . n = h . (n + 1)
proof
let n be Nat; :: thesis: g . n = h . (n + 1)
n in NAT by ORDINAL1:def 12;
then ex m being Nat st
( m = n & g . n = h . (m + 1) ) by A77;
hence g . n = h . (n + 1) ; :: thesis: verum
end;
rng g c= F1()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in F1() )
assume x in rng g ; :: thesis: x in F1()
then consider y being object such that
A80: y in dom g and
A81: x = g . y by FUNCT_1:def 3;
reconsider k = y as Nat by ;
k + 1 in dom h by A44;
then A82: h . (k + 1) in rng h by FUNCT_1:def 3;
x = h . (k + 1) by ;
hence x in F1() by ; :: thesis: verum
end;
then reconsider g = g as sequence of F1() by ;
A83: for n being Nat holds g . n = h . (n + 1) by A79;
A84: for n being Nat st n + 2 <= len <*F2()*> holds
<*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))]
proof
let n be Nat; :: thesis: ( n + 2 <= len <*F2()*> implies <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] )
assume n + 2 <= len <*F2()*> ; :: thesis: <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))]
then (n + 1) + 1 <= 0 + 1 by FINSEQ_1:39;
then n + 1 <= 0 by XREAL_1:6;
then n + 1 <= 0 + n ;
hence <*F2()*> . (n + 2) = f . [n,(<*F2()*> . (n + 1))] by XREAL_1:6; :: thesis: verum
end;
( <*F2()*> in F1() * & <*F2()*> . 1 = F2() ) by ;
then <*F2()*> in X by ;
then A85: {[1,F2()]} in X by FINSEQ_1:37;
take g ; :: thesis: ( g . 0 = F2() & ( for n being Nat holds P1[n,g . n,g . (n + 1)] ) )
[1,F2()] in {[1,F2()]} by TARSKI:def 1;
then [1,F2()] in h by ;
then F2() = h . (0 + 1) by FUNCT_1:1
.= g . 0 by A83 ;
hence g . 0 = F2() ; :: thesis: for n being Nat holds P1[n,g . n,g . (n + 1)]
let n be Nat; :: thesis: P1[n,g . n,g . (n + 1)]
A86: h . (n + (1 + 1)) = f . (n,(h . (n + 1))) by A70;
A87: n in NAT by ORDINAL1:def 12;
then g . n in F1() by FUNCT_2:5;
then P1[n,g . n,f . (n,(g . n))] by ;
then P1[n,g . n,h . ((n + 1) + 1)] by ;
hence P1[n,g . n,g . (n + 1)] by A83; :: thesis: verum