let ti be INT-Expression of A,f; :: thesis: ( ti = t1 mod t2 iff for s being Element of Funcs (X,INT) holds ti . s = (t1 . s) mod (t2 . s) )

A5: dom t1 = Funcs (X,INT) by FUNCT_2:def 1;

A6: dom t2 = Funcs (X,INT) by FUNCT_2:def 1;

A7: dom (t1 mod t2) = (dom t1) /\ (dom t2) by Def4;

hence ( ti = t1 mod t2 implies for s being Element of Funcs (X,INT) holds ti . s = (t1 . s) mod (t2 . s) ) by A5, A6, Def4; :: thesis: ( ( for s being Element of Funcs (X,INT) holds ti . s = (t1 . s) mod (t2 . s) ) implies ti = t1 mod t2 )

A8: dom ti = Funcs (X,INT) by FUNCT_2:def 1;

assume for s being Element of Funcs (X,INT) holds ti . s = (t1 . s) mod (t2 . s) ; :: thesis: ti = t1 mod t2

then for s being object st s in Funcs (X,INT) holds

ti . s = (t1 . s) mod (t2 . s) ;

hence ti = t1 mod t2 by A7, A5, A6, A8, Def4; :: thesis: verum

A5: dom t1 = Funcs (X,INT) by FUNCT_2:def 1;

A6: dom t2 = Funcs (X,INT) by FUNCT_2:def 1;

A7: dom (t1 mod t2) = (dom t1) /\ (dom t2) by Def4;

hence ( ti = t1 mod t2 implies for s being Element of Funcs (X,INT) holds ti . s = (t1 . s) mod (t2 . s) ) by A5, A6, Def4; :: thesis: ( ( for s being Element of Funcs (X,INT) holds ti . s = (t1 . s) mod (t2 . s) ) implies ti = t1 mod t2 )

A8: dom ti = Funcs (X,INT) by FUNCT_2:def 1;

assume for s being Element of Funcs (X,INT) holds ti . s = (t1 . s) mod (t2 . s) ; :: thesis: ti = t1 mod t2

then for s being object st s in Funcs (X,INT) holds

ti . s = (t1 . s) mod (t2 . s) ;

hence ti = t1 mod t2 by A7, A5, A6, A8, Def4; :: thesis: verum