let F, G be Function of (X1 union X2),Y; :: thesis: ( F | X1 = f1 & F | X2 = f2 & G | X1 = f1 & G | X2 = f2 implies F = G )
assume that
A9: ( F | X1 = f1 & F | X2 = f2 ) and
A10: ( G | X1 = f1 & G | X2 = f2 ) ; :: thesis: F = G
A11: ( X1 is SubSpace of X1 union X2 & X2 is SubSpace of X1 union X2 ) by TSEP_1:22;
set A1 = the carrier of X1;
set A2 = the carrier of X2;
set A = the carrier of (X1 union X2);
A12: the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def 2;

now

let a be Element of the carrier of (X1 union X2); :: thesis: F . a = G . a

A13: now

assume A14: a in the carrier of X1 ; :: thesis: F . a = G . a
hence F . a = (F | the carrier of X1) . a by FUNCT_1:72
.= f1 . a by A9, A11, Def4
.= (G | the carrier of X1) . a by A10, A11, Def4
.= G . a by A14, FUNCT_1:72 ;
:: thesis: verum

end;

now

assume A15: a in the carrier of X2 ; :: thesis: F . a = G . a
hence F . a = (F | the carrier of X2) . a by FUNCT_1:72
.= f2 . a by A9, A11, Def4
.= (G | the carrier of X2) . a by A10, A11, Def4
.= G . a by A15, FUNCT_1:72 ;
:: thesis: verum

end;

hence F . a = G . a by A12, A13, XBOOLE_0:def 3; :: thesis: verum

end;

hence F = G by FUNCT_2:113; :: thesis: verum