deffunc H₂( Nat) -> Element of the U1 of X = (Cseq . $1) * (seq . $1);
consider M being sequence of X such that
A1: for n being Element of NAT holds M . n = H₂(n) from FUNCT_2:sch 4();
take M ; :: thesis: for n being Nat holds M . n = (Cseq . n) * (seq . n)
let n be Nat; :: thesis: M . n = (Cseq . n) * (seq . n)
n in NAT by ORDINAL1:def 12;
hence M . n = (Cseq . n) * (seq . n) by A1; :: thesis: verum