let ti be INT-Expression of A,f; :: thesis: ( ti = leq t1,t2 iff for s being Element of Funcs X,INT holds ti . s = IFGT (t1 . s),(t2 . s),0 ,1 )
A9: dom t1 = Funcs X,INT by FUNCT_2:def 1;
A10: dom t2 = Funcs X,INT by FUNCT_2:def 1;
A11: dom (leq t1,t2) = (dom t1) /\ (dom t2) by Def5;
hence ( ti = leq t1,t2 implies for s being Element of Funcs X,INT holds ti . s = IFGT (t1 . s),(t2 . s),0 ,1 ) by A9, A10, Def5; :: thesis: ( ( for s being Element of Funcs X,INT holds ti . s = IFGT (t1 . s),(t2 . s),0 ,1 ) implies ti = leq t1,t2 )
A12: 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),0 ,1 ; :: thesis: ti = leq t1,t2
then for s being set st s in Funcs X,INT holds
ti . s = IFGT (t1 . s),(t2 . s),0 ,1 ;
hence ti = leq t1,t2 by A11, A9, A10, A12, Def5; :: thesis: verum