let F, G be Element of QC-WFF ; :: thesis: ( F is_subformula_of G & len (@ F) = len (@ G) implies F = G )
assume that
A1: F is_subformula_of G and
A2: len (@ F) = len (@ G) ; :: thesis: F = G

now

assume F <> G ; :: thesis: contradiction
then F is_proper_subformula_of G by A1, QC_LANG2:def 21;
hence contradiction by A2, QC_LANG2:54; :: thesis: verum

end;

hence F = G ; :: thesis: verum