defpred S1[ Nat, set , set ] means ( ( $2 is NatRelStr of (3 * (2 |^ $1)) -' 1 implies ex R being NatRelStr of (3 * (2 |^ $1)) -' 1 st
( $2 = R & $3 = Mycielskian R ) ) & ( $2 is not NatRelStr of (3 * (2 |^ $1)) -' 1 implies $3 = $2 ) );
P: for n being Element of NAT
for x being set ex y being set st S1[n,x,y]
proof
let n be Element of NAT ; :: thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; :: thesis: ex y being set st S1[n,x,y]
per cases ( x is NatRelStr of (3 * (2 |^ n)) -' 1 or not x is NatRelStr of (3 * (2 |^ n)) -' 1 ) ;
suppose x is NatRelStr of (3 * (2 |^ n)) -' 1 ; :: thesis: ex y being set st S1[n,x,y]
then reconsider R = x as NatRelStr of (3 * (2 |^ n)) -' 1 ;
Mycielskian R = Mycielskian R ;
hence ex y being set st S1[n,x,y] ; :: thesis: verum
end;
suppose x is not NatRelStr of (3 * (2 |^ n)) -' 1 ; :: thesis: ex y being set st S1[n,x,y]
hence ex y being set st S1[n,x,y] ; :: thesis: verum
end;
end;
end;
consider f being Function such that
A: dom f = NAT and
B: f . 0 = CompleteRelStr 2 and
C: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(P);
 defpred S2[ Nat] means f . $1 is NatRelStr of (3 * (2 |^ $1)) -' 1;
(3 * (2 |^ 0)) -' 1 = (3 * 1) -' 1 by NEWTON:9
.= (2 + 1) -' 1
.= 2 by NAT_D:34 ;
then P1: S2[ 0 ] by B;
P2: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A1: S2[k] ; :: thesis: S2[k + 1]
consider R being NatRelStr of (3 * (2 |^ k)) -' 1 such that
f . k = R and
C1: f . (k + 1) = Mycielskian R by A1, C;
D1aa: 3 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:66;
( 2 |^ k >= k + 1 & k + 1 >= 1 ) by NEWTON:104, NAT_1:11;
then 2 |^ k >= 1 by XXREAL_0:2;
then D1ab: 3 * (2 |^ k) >= 1 by D1aa, XXREAL_0:2;
then D1a: (3 * (2 |^ k)) - 1 >= 1 - 1 by XREAL_1:11;
2 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:66;
then 2 |^ (k + 1) >= 2 |^ k by NEWTON:11;
then 3 * (2 |^ (k + 1)) >= 3 * (2 |^ k) by XREAL_1:66;
then 3 * (2 |^ (k + 1)) >= 1 by D1ab, XXREAL_0:2;
then D1b: (3 * (2 |^ (k + 1))) - 1 >= 1 - 1 by XREAL_1:11;
(2 * ((3 * (2 |^ k)) -' 1)) + 1 = (2 * ((3 * (2 |^ k)) - 1)) + 1 by D1a, XREAL_0:def 2
.= ((3 * (2 * (2 |^ k))) - 2) + 1
.= ((3 * (2 |^ (k + 1))) - 2) + 1 by NEWTON:11
.= (3 * (2 |^ (k + 1))) -' 1 by D1b, XREAL_0:def 2 ;
hence S2[k + 1] by C1; :: thesis: verum
end;
D: for n being Element of NAT holds S2[n] from NAT_1:sch 1(P1, P2);
 n is Element of NAT by ORDINAL1:def 13;
then reconsider IT = f . n as NatRelStr of (3 * (2 |^ n)) -' 1 by D;
take IT ; :: thesis: ex myc being Function st
( IT = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) )
take myc = f; :: thesis: ( IT = myc . n & dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) )
thus IT = myc . n ; :: thesis: ( dom myc = NAT & myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) )
thus dom myc = NAT by A; :: thesis: ( myc . 0 = CompleteRelStr 2 & ( for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R ) )
thus myc . 0 = CompleteRelStr 2 by B; :: thesis: for k being Nat
for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R
let k be Nat; :: thesis: for R being NatRelStr of (3 * (2 |^ k)) -' 1 st R = myc . k holds
myc . (k + 1) = Mycielskian R
E: k is Element of NAT by ORDINAL1:def 13;
let R be NatRelStr of (3 * (2 |^ k)) -' 1; :: thesis: ( R = myc . k implies myc . (k + 1) = Mycielskian R )
assume A1: R = myc . k ; :: thesis: myc . (k + 1) = Mycielskian R
then consider RR being NatRelStr of (3 * (2 |^ k)) -' 1 such that
F: f . k = RR and
G: f . (k + 1) = Mycielskian RR by E, C;
thus myc . (k + 1) = Mycielskian R by G, A1, F; :: thesis: verum