let U be non empty set ; :: thesis: (U -deltaInterpreter) " {1} = (U -concatenation) .: (id (1 -tuples_on U))
set d = U -deltaInterpreter ;
set f = U -concatenation ;
set U1 = 1 -tuples_on U;
set U2 = 2 -tuples_on U;
set A = (U -concatenation) .: (id (1 -tuples_on U));
set B = 2 -tuples_on U;
A1: (U -deltaInterpreter) " {1} = ((U -concatenation) .: (id (1 -tuples_on U))) /\ ((1 + 1) -tuples_on U) by FOMODEL0:24
.= ((U -concatenation) .: (id (1 -tuples_on U))) /\ ((U -concatenation) .: [:(1 -tuples_on U),(1 -tuples_on U):]) by FOMODEL0:22 ;
reconsider O = (U -concatenation) .: (id (1 -tuples_on U)) as Subset of ((U -concatenation) .: [:(1 -tuples_on U),(1 -tuples_on U):]) by RELAT_1:123;
O /\ ((U -concatenation) .: [:(1 -tuples_on U),(1 -tuples_on U):]) = O null ((U -concatenation) .: [:(1 -tuples_on U),(1 -tuples_on U):])
.= O ;
hence (U -deltaInterpreter) " {1} = (U -concatenation) .: (id (1 -tuples_on U)) by A1; :: thesis: verum