let IT be Function of A,BOOLEAN; :: thesis: ( IT = p 'imp' q iff for x being Element of A holds IT . x = ('not' (p . x)) 'or' (q . x) )
A2: dom q = A by FUNCT_2:def 1;

hereby :: thesis: ( ( for x being Element of A holds IT . x = ('not' (p . x)) 'or' (q . x) ) implies IT = p 'imp' q )

assume A3: IT = p 'imp' q ; :: thesis: for x being Element of A holds IT . x = ('not' (p . x)) 'or' (q . x)
let x be Element of A; :: thesis: IT . x = ('not' (p . x)) 'or' (q . x)
( dom p = A & dom q = A ) by FUNCT_2:def 1;
then dom (p 'imp' q) = A /\ A by Def6
.= A ;
hence IT . x = (p . x) => (q . x) by A3, Def6
.= ('not' (p . x)) 'or' (q . x) ;
:: thesis: verum

end;

assume A4: for x being Element of A holds IT . x = ('not' (p . x)) 'or' (q . x) ; :: thesis: IT = p 'imp' q
A5: for x being set st x in dom IT holds
IT . x = (p . x) => (q . x)

proof

let x be set ; :: thesis: ( x in dom IT implies IT . x = (p . x) => (q . x) )
assume x in dom IT ; :: thesis: IT . x = (p . x) => (q . x)
then reconsider x = x as Element of A by FUNCT_2:def 1;
IT . x = ('not' (p . x)) 'or' (q . x) by A4;
hence IT . x = (p . x) => (q . x) ; :: thesis: verum

end;

dom IT = A /\ A by FUNCT_2:def 1
.= (dom p) /\ (dom q) by A2, FUNCT_2:def 1 ;
hence IT = p 'imp' q by A5, Def6; :: thesis: verum