let n be Nat; :: thesis: ( n >= 3 implies U3(n)Turing computes n proj 3 )
assume A1: n >= 3 ; :: thesis:
now :: thesis: for s being All-State of U3(n)Turing
for t being Tape of U3(n)Turing
for h being Element of NAT
for x being FinSequence of NAT st x in dom (n proj 3) & s = [ the InitS of U3(n)Turing,h,t] & t storeData <*h*> ^ x holds
( s is Accept-Halt & ex h2 being Element of omega ex y being Element of NAT st
( () `2_3 = h2 & y = (n proj 3) . x & () `3_3 storeData <*h2*> ^ <*y*> ) )
set pj = n proj 3;
let s be All-State of U3(n)Turing; :: thesis: for t being Tape of U3(n)Turing
for h being Element of NAT
for x being FinSequence of NAT st x in dom (n proj 3) & s = [ the InitS of U3(n)Turing,h,t] & t storeData <*h*> ^ x holds
( s is Accept-Halt & ex h2 being Element of omega ex y being Element of NAT st
( () `2_3 = h2 & y = (n proj 3) . x & () `3_3 storeData <*h2*> ^ <*y*> ) )

let t be Tape of U3(n)Turing; :: thesis: for h being Element of NAT
for x being FinSequence of NAT st x in dom (n proj 3) & s = [ the InitS of U3(n)Turing,h,t] & t storeData <*h*> ^ x holds
( s is Accept-Halt & ex h2 being Element of omega ex y being Element of NAT st
( () `2_3 = h2 & y = (n proj 3) . x & () `3_3 storeData <*h2*> ^ <*y*> ) )

let h be Element of NAT ; :: thesis: for x being FinSequence of NAT st x in dom (n proj 3) & s = [ the InitS of U3(n)Turing,h,t] & t storeData <*h*> ^ x holds
( s is Accept-Halt & ex h2 being Element of omega ex y being Element of NAT st
( () `2_3 = h2 & y = (n proj 3) . x & () `3_3 storeData <*h2*> ^ <*y*> ) )

let x be FinSequence of NAT ; :: thesis: ( x in dom (n proj 3) & s = [ the InitS of U3(n)Turing,h,t] & t storeData <*h*> ^ x implies ( s is Accept-Halt & ex h2 being Element of omega ex y being Element of NAT st
( () `2_3 = h2 & y = (n proj 3) . x & () `3_3 storeData <*h2*> ^ <*y*> ) ) )

assume that
A2: x in dom (n proj 3) and
A3: s = [ the InitS of U3(n)Turing,h,t] and
A4: t storeData <*h*> ^ x ; :: thesis: ( s is Accept-Halt & ex h2 being Element of omega ex y being Element of NAT st
( () `2_3 = h2 & y = (n proj 3) . x & () `3_3 storeData <*h2*> ^ <*y*> ) )

reconsider nn = n as Element of NAT by ORDINAL1:def 12;
set pj = nn proj 3;
arity (nn proj 3) = n by COMPUT_1:37;
then A5: dom (nn proj 3) c= n -tuples_on NAT by COMPUT_1:21;
then x in n -tuples_on NAT by A2;
then x in { f where f is Element of NAT * : len f = n } by FINSEQ_2:def 4;
then A6: ex f being Element of NAT * st
( x = f & len f = n ) ;
A7: s = [0,h,t] by ;
hence s is Accept-Halt by A1, A4, A6, Th37; :: thesis: ex h2 being Element of omega ex y being Element of NAT st
( () `2_3 = h2 & y = (n proj 3) . x & () `3_3 storeData <*h2*> ^ <*y*> )

take h2 = ((h + (x /. 1)) + (x /. 2)) + 4; :: thesis: ex y being Element of NAT st
( () `2_3 = h2 & y = (n proj 3) . x & () `3_3 storeData <*h2*> ^ <*y*> )

take y = x /. 3; :: thesis: ( () `2_3 = h2 & y = (n proj 3) . x & () `3_3 storeData <*h2*> ^ <*y*> )
thus (Result s) `2_3 = h2 by A1, A4, A6, A7, Th37; :: thesis: ( y = (n proj 3) . x & () `3_3 storeData <*h2*> ^ <*y*> )
thus y = x . 3 by
.= (nn proj 3) . x by
.= (n proj 3) . x ; :: thesis: () `3_3 storeData <*h2*> ^ <*y*>
(Result s) `3_3 storeData <*h2,y*> by A1, A4, A6, A7, Th37;
hence (Result s) `3_3 storeData <*h2*> ^ <*y*> ; :: thesis: verum
end;
hence U3(n)Turing computes n proj 3 ; :: thesis: verum