let p be Element of HP-WFF ; :: thesis: ( p . 1 = 0 implies p = VERUM )
assume A1: p . 1 = 0 ; :: thesis: p = VERUM

per cases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;

suppose p is conjunctive ; :: thesis: p = VERUM

then consider r, s being Element of HP-WFF such that
A2: p = r '&' s by Def6;
p = <*2*> ^ (r ^ s) by A2, FINSEQ_1:45;
hence p = VERUM by A1, FINSEQ_1:58; :: thesis: verum

end;

suppose p is conditional ; :: thesis: p = VERUM

then consider r, s being Element of HP-WFF such that
A3: p = r => s by Def7;
p = <*1*> ^ (r ^ s) by A3, FINSEQ_1:45;
hence p = VERUM by A1, FINSEQ_1:58; :: thesis: verum

end;

suppose p is simple ; :: thesis: p = VERUM

then consider n being Element of NAT such that
A4: p = prop n by Def8;
thus p = VERUM by A1, A4, FINSEQ_1:57; :: thesis: verum

end;

suppose p = VERUM ; :: thesis: p = VERUM

hence p = VERUM ; :: thesis: verum

end;

end;