defpred S₁[ Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)), Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))] means for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = ($1 . i) . j & ($2 . i) . j = (SBT ") . inputij );
A1: for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S₁[text,z]

proof

let text be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S₁[text,z]
text in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then Q01: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( text = s & len s = 4 ) ;
defpred S₂[ Nat, set ] means ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( $2 = zk & ( for j being Nat st j in Seg 4 holds
ex textij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . $1) . j & zk . j = (SBT ") . textij ) ) );
Q1: for k being Nat st k in Seg 4 holds
ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S₂[k,zk]

proof

let k be Nat; :: thesis: ( k in Seg 4 implies ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S₂[k,zk] )
assume k in Seg 4 ; :: thesis: ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S₂[k,zk]
then k in dom text by Q01, FINSEQ_1:def 3;
then text . k in rng text by FUNCT_1:3;
then text . k in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then Q13: ex s being Element of (8 -tuples_on BOOLEAN) * st
( text . k = s & len s = 4 ) ;
then reconsider textk = text . k as Element of (8 -tuples_on BOOLEAN) * ;
defpred S₃[ Nat, set ] means ex textij being Element of 8 -tuples_on BOOLEAN st
( textij = textk . $1 & $2 = (SBT ") . textij );
Q18: for j being Nat st j in Seg 4 holds
ex xi being Element of 8 -tuples_on BOOLEAN st S₃[j,xi]

proof

let j be Nat; :: thesis: ( j in Seg 4 implies ex xi being Element of 8 -tuples_on BOOLEAN st S₃[j,xi] )
assume j in Seg 4 ; :: thesis: ex xi being Element of 8 -tuples_on BOOLEAN st S₃[j,xi]
then j in dom textk by Q13, FINSEQ_1:def 3;
then textk . j in rng textk by FUNCT_1:3;
then reconsider textkj = textk . j as Element of 8 -tuples_on BOOLEAN ;
(SBT ") . textkj = (SBT ") . textkj ;
hence ex xi being Element of 8 -tuples_on BOOLEAN st S₃[j,xi] ; :: thesis: verum

end;

consider zk being FinSequence of 8 -tuples_on BOOLEAN such that
Q22: ( dom zk = Seg 4 & ( for j being Nat st j in Seg 4 holds
S₃[j,zk . j] ) ) from FINSEQ_1:sch 5(Q18);
Q23: len zk = 4 by Q22, FINSEQ_1:def 3;
reconsider zk = zk as Element of (8 -tuples_on BOOLEAN) * by FINSEQ_1:def 11;
zk in 4 -tuples_on (8 -tuples_on BOOLEAN) by Q23;
then reconsider zk = zk as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
for j being Nat st j in Seg 4 holds
ex textij being Element of 8 -tuples_on BOOLEAN st
( textij = textk . j & zk . j = (SBT ") . textij ) by Q22;
hence ex zk being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S₂[k,zk] ; :: thesis: verum

end;

consider z being FinSequence of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
Q2: ( dom z = Seg 4 & ( for i being Nat st i in Seg 4 holds
S₂[i,z . i] ) ) from FINSEQ_1:sch 5(Q1);
Q3: len z = 4 by Q2, FINSEQ_1:def 3;
reconsider z = z as Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * by FINSEQ_1:def 11;
z in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by Q3;
then reconsider z = z as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
take z ; :: thesis: S₁[text,z]
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & (z . i) . j = (SBT ") . textij )

proof

let i, j be Nat; :: thesis: ( i in Seg 4 & j in Seg 4 implies ex textij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & (z . i) . j = (SBT ") . textij ) )
assume Q4: ( i in Seg 4 & j in Seg 4 ) ; :: thesis: ex textij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & (z . i) . j = (SBT ") . textij )
then ex zi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( z . i = zi & ( for j being Nat st j in Seg 4 holds
ex textij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & zi . j = (SBT ") . textij ) ) ) by Q2;
hence ex textij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & (z . i) . j = (SBT ") . textij ) by Q4; :: thesis: verum

end;

hence S₁[text,z] ; :: thesis: verum

end;

consider I being Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) such that
A2: for x being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds S₁[x,I . x] from FUNCT_2:sch 3(A1);
take I ; :: thesis: for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((I . input) . i) . j = (SBT ") . inputij )
thus for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex inputij being Element of 8 -tuples_on BOOLEAN st
( inputij = (input . i) . j & ((I . input) . i) . j = (SBT ") . inputij ) by A2; :: thesis: verum