let ti be INT-Expression of A,f; :: thesis: ( ti = gt (t1,t2) iff for s being Element of Funcs (X,INT) holds ti . s = IFGT ((t1 . s),(t2 . s),1,0) )
A13: dom t1 = Funcs (X,INT) by FUNCT_2:def 1;
A14: dom t2 = Funcs (X,INT) by FUNCT_2:def 1;
A15: dom (gt (t1,t2)) = (dom t1) /\ (dom t2) by Def6;
hence ( ti = gt (t1,t2) implies for s being Element of Funcs (X,INT) holds ti . s = IFGT ((t1 . s),(t2 . s),1,0) ) by A13, A14, Def6; :: thesis: ( ( for s being Element of Funcs (X,INT) holds ti . s = IFGT ((t1 . s),(t2 . s),1,0) ) implies ti = gt (t1,t2) )
A16: dom ti = Funcs (X,INT) by FUNCT_2:def 1;
assume for s being Element of Funcs (X,INT) holds ti . s = IFGT ((t1 . s),(t2 . s),1,0) ; :: thesis: ti = gt (t1,t2)
then for s being object st s in Funcs (X,INT) holds
ti . s = IFGT ((t1 . s),(t2 . s),1,0) ;
hence ti = gt (t1,t2) by A15, A13, A14, A16, Def6; :: thesis: verum