let A be QC-alphabet ; :: thesis: for F, G being Element of QC-WFF A st F is_subformula_of G & len (@ F) = len (@ G) holds
F = G
let F, G be Element of QC-WFF A; :: 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 :: thesis: not F <> G

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