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 ) );
A1: 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
A2: dom f = NAT and
A3: f . 0 = CompleteRelStr 2 and
A4: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch 1(A1);
 defpred S2[ Nat] means f . $1 is NatRelStr of (3 * (2 |^ $1)) -' 1;
(3 * (2 |^ 0)) -' 1 = (3 * 1) -' 1 by NEWTON:4
.= (2 + 1) -' 1
.= 2 by NAT_D:34 ;
then A5: S2[ 0 ] by A3;
A6: 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 A7: S2[k] ; :: thesis: S2[k + 1]
consider R being NatRelStr of (3 * (2 |^ k)) -' 1 such that
f . k = R and
A8: f . (k + 1) = Mycielskian R by A7, A4;
A9: 3 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;
( 2 |^ k >= k + 1 & k + 1 >= 1 ) by NAT_1:11, NEWTON:85;
then 2 |^ k >= 1 by XXREAL_0:2;
then A10: 3 * (2 |^ k) >= 1 by A9, XXREAL_0:2;
then A11: (3 * (2 |^ k)) - 1 >= 1 - 1 by XREAL_1:9;
2 * (2 |^ k) >= 1 * (2 |^ k) by XREAL_1:64;
then 2 |^ (k + 1) >= 2 |^ k by NEWTON:6;
then 3 * (2 |^ (k + 1)) >= 3 * (2 |^ k) by XREAL_1:64;
then 3 * (2 |^ (k + 1)) >= 1 by A10, XXREAL_0:2;
then A12: (3 * (2 |^ (k + 1))) - 1 >= 1 - 1 by XREAL_1:9;
(2 * ((3 * (2 |^ k)) -' 1)) + 1 = (2 * ((3 * (2 |^ k)) - 1)) + 1 by A11, XREAL_0:def 2
.= ((3 * (2 * (2 |^ k))) - 2) + 1
.= ((3 * (2 |^ (k + 1))) - 2) + 1 by NEWTON:6
.= (3 * (2 |^ (k + 1))) -' 1 by A12, XREAL_0:def 2 ;
hence S2[k + 1] by A8; :: thesis: verum
end;
A13: for n being Element of NAT holds S2[n] from NAT_1:sch 1(A5, A6);
 n is Element of NAT by ORDINAL1:def 12;
then reconsider IT = f . n as NatRelStr of (3 * (2 |^ n)) -' 1 by A13;
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 A2; :: 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 A3; :: 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
A14: k is Element of NAT by ORDINAL1:def 12;
let R be NatRelStr of (3 * (2 |^ k)) -' 1; :: thesis: ( R = myc . k implies myc . (k + 1) = Mycielskian R )
assume A15: R = myc . k ; :: thesis: myc . (k + 1) = Mycielskian R
then consider RR being NatRelStr of (3 * (2 |^ k)) -' 1 such that
A16: f . k = RR and
A17: f . (k + 1) = Mycielskian RR by A14, A4;
thus myc . (k + 1) = Mycielskian R by A17, A15, A16; :: thesis: verum