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

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