A3: ex S being non empty ManySortedSign ex x being set st
( S = F₄() . 0 & x = F₅() . 0 & S₁[S,x, 0 ] ) by A1;
let n be Nat; :: thesis: for x being set st x = F₅() . n holds
F₅() . (n + 1) = F₃(x,n)
let x be set ; :: thesis: ( x = F₅() . n implies F₅() . (n + 1) = F₃(x,n) )
A4: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F₄() . n & x = F₅() . n & S₁[S,x,n] holds
S₁[F₂(S,x,n),F₃(x,n),n + 1] ;
A5: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F₄() . n & x = F₅() . n holds
( F₄() . (n + 1) = F₂(S,x,n) & F₅() . (n + 1) = F₃(x,n) ) by A2;
for n being Nat ex S being non empty ManySortedSign st
( S = F₄() . n & S₁[S,F₅() . n,n] ) from CIRCCMB2:sch 2(A3, A5, A4);
then A6: ex S being non empty ManySortedSign st S = F₄() . n ;
assume x = F₅() . n ; :: thesis: F₅() . (n + 1) = F₃(x,n)
hence F₅() . (n + 1) = F₃(x,n) by A2, A6; :: thesis: verum