deffunc H₁( set , set ) -> QC-symbol of A = ($2 @ A) ++ ;
consider f being sequence of (QC-symbols A) such that
A1: ( f . 0 = t & ( for k being Nat holds f . (k + 1) = H₁(k,f . k) ) ) from NAT_1:sch 12();
take f . n ; :: thesis: ex f being sequence of (QC-symbols A) st
( f . n = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) )
for k being Nat holds f . (k + 1) = (f . k) ++

proof

let k be Nat; :: thesis: f . (k + 1) = (f . k) ++
( (f . k) ++ = H₁(k,f . k) & H₁(k,f . k) = f . (k + 1) ) by A1, Def39;
hence f . (k + 1) = (f . k) ++ ; :: thesis: verum

end;

hence ex f being sequence of (QC-symbols A) st
( f . n = f . n & f . 0 = t & ( for k being Nat holds f . (k + 1) = (f . k) ++ ) ) by A1; :: thesis: verum