A3:
ex S being non empty ManySortedSign ex x being set st

( S = F_{4}() . 0 & x = F_{5}() . 0 & S_{1}[S,x, 0 ] )
by A1;

let n be Nat; :: thesis: for x being set st x = F_{5}() . n holds

F_{5}() . (n + 1) = F_{3}(x,n)

let x be set ; :: thesis: ( x = F_{5}() . n implies F_{5}() . (n + 1) = F_{3}(x,n) )

A4: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F_{4}() . n & x = F_{5}() . n & S_{1}[S,x,n] holds

S_{1}[F_{2}(S,x,n),F_{3}(x,n),n + 1]
;

A5: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F_{4}() . n & x = F_{5}() . n holds

( F_{4}() . (n + 1) = F_{2}(S,x,n) & F_{5}() . (n + 1) = F_{3}(x,n) )
by A2;

for n being Nat ex S being non empty ManySortedSign st

( S = F_{4}() . n & S_{1}[S,F_{5}() . n,n] )
from CIRCCMB2:sch 2(A3, A5, A4);

then A6: ex S being non empty ManySortedSign st S = F_{4}() . n
;

assume x = F_{5}() . n
; :: thesis: F_{5}() . (n + 1) = F_{3}(x,n)

hence F_{5}() . (n + 1) = F_{3}(x,n)
by A2, A6; :: thesis: verum

( S = F

let n be Nat; :: thesis: for x being set st x = F

F

let x be set ; :: thesis: ( x = F

A4: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F

S

A5: for n being Nat

for S being non empty ManySortedSign

for x being set st S = F

( F

for n being Nat ex S being non empty ManySortedSign st

( S = F

then A6: ex S being non empty ManySortedSign st S = F

assume x = F

hence F