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 A1: ( ( 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 ) ) ; :: thesis: F1 = F2
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
( F1 = modid X,C & F2 = modid X,C ) by A1;
hence F1 = F2 ; :: thesis: verum