reconsider B = the carrier of X0 as Subset of X by TSEP_1:1;

reconsider F = modid (X,B) as Function of X,(X modified_with_respect_to X0) by Def10;

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

reconsider F = modid (X,B) as Function of X,(X modified_with_respect_to X0) by Def10;

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