reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
let F1, F2 be Function of X,(X modified_with_respect_to X0); :: thesis: ( ( for A being Subset of X st A = the carrier of X0 holds
F1 = modid (X,A) ) & ( for A being Subset of X st A = the carrier of X0 holds
F2 = modid (X,A) ) implies F1 = F2 )
assume that
A1: for A being Subset of X st A = the carrier of X0 holds
F1 = modid (X,A) and
A2: for A being Subset of X st A = the carrier of X0 holds
F2 = modid (X,A) ; :: thesis: F1 = F2
F1 = modid (X,C) by A1;
hence F1 = F2 by A2; :: thesis: verum