Sub | X = (@ Sub) | X ;
hence Sub | X is CQC_Substitution of A by PARTFUN1:45; :: thesis: verum