let ti be INT-Expression of A,f; :: thesis: ( ti = t1 div t2 iff for s being Element of Funcs (X,INT) holds ti . s = (t1 . s) div (t2 . s) )
A1: dom t1 = Funcs (X,INT) by FUNCT_2:def 1;
A2: dom t2 = Funcs (X,INT) by FUNCT_2:def 1;
A3: dom (t1 div t2) = (dom t1) /\ (dom t2) by Def3;
hence ( ti = t1 div t2 implies for s being Element of Funcs (X,INT) holds ti . s = (t1 . s) div (t2 . s) ) by A1, A2, Def3; :: thesis: ( ( for s being Element of Funcs (X,INT) holds ti . s = (t1 . s) div (t2 . s) ) implies ti = t1 div t2 )
A4: dom ti = Funcs (X,INT) by FUNCT_2:def 1;
assume for s being Element of Funcs (X,INT) holds ti . s = (t1 . s) div (t2 . s) ; :: thesis: ti = t1 div t2
then for s being object st s in Funcs (X,INT) holds
ti . s = (t1 . s) div (t2 . s) ;
hence ti = t1 div t2 by A3, A1, A2, A4, Def3; :: thesis: verum