reconsider B = the carrier of X0 as Subset of X by TSEP_1:1;
X modified_with_respect_to B = X modified_with_respect_to X0 by Def10;
then reconsider F = modid X,B as Function of X,(X modified_with_respect_to X0) ;
take F ; :: thesis: for A being Subset of X st A = the carrier of X0 holds
F = modid X,A
thus for A being Subset of X st A = the carrier of X0 holds
F = modid X,A ; :: thesis: verum