set a = SC_assignment (f,v);
reconsider d1 = d as TypeSCNominativeData of V,A ;

per cases ( d in dom (SC_assignment (f,v)) or not d in dom (SC_assignment (f,v)) ) ;

suppose d in dom (SC_assignment (f,v)) ; :: thesis: ( (SC_assignment (f,v)) . d is Function-like & (SC_assignment (f,v)) . d is Relation-like )

then (SC_assignment (f,v)) . d1 = local_overlapping (V,A,d1,(f . d1),v) by Def7;
hence ( (SC_assignment (f,v)) . d is Function-like & (SC_assignment (f,v)) . d is Relation-like ) ; :: thesis: verum

end;

suppose not d in dom (SC_assignment (f,v)) ; :: thesis: ( (SC_assignment (f,v)) . d is Function-like & (SC_assignment (f,v)) . d is Relation-like )

hence ( (SC_assignment (f,v)) . d is Function-like & (SC_assignment (f,v)) . d is Relation-like ) by FUNCT_1:def 2; :: thesis: verum

end;

end;