set A = the carrier of (X1 union X2);
A9: X2 is SubSpace of X1 union X2 by TSEP_1:22;
set A2 = the carrier of X2;
A10: X1 is SubSpace of X1 union X2 by TSEP_1:22;
set A1 = the carrier of X1;
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
A11: F | X1 = f1 and
A12: F | X2 = f2 and
A13: G | X1 = f1 and
A14: G | X2 = f2 ; :: thesis: F = G
A15: the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def 2;
now :: thesis: for a being Element of the carrier of (X1 union X2) holds F . a = G . a
let a be Element of the carrier of (X1 union X2); :: thesis: F . a = G . a
A16: now :: thesis: ( a in the carrier of X2 implies F . a = G . a )
assume A17: a in the carrier of X2 ; :: thesis: F . a = G . a
hence F . a = (F | the carrier of X2) . a by FUNCT_1:49
.= f2 . a by A12, A9, Def5
.= (G | the carrier of X2) . a by A14, A9, Def5
.= G . a by A17, FUNCT_1:49 ;
:: thesis: verum
end;
now :: thesis: ( a in the carrier of X1 implies F . a = G . a )
assume A18: a in the carrier of X1 ; :: thesis: F . a = G . a
hence F . a = (F | the carrier of X1) . a by FUNCT_1:49
.= f1 . a by A11, A10, Def5
.= (G | the carrier of X1) . a by A13, A10, Def5
.= G . a by A18, FUNCT_1:49 ;
:: thesis: verum
end;
hence F . a = G . a by A15, A16, XBOOLE_0:def 3; :: thesis: verum
end;
hence F = G by FUNCT_2:63; :: thesis: verum