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;

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

hence
F = G
by FUNCT_2:63; :: thesis: verumlet a be Element of the carrier of (X1 union X2); :: thesis: F . a = G . a

end;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;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

now :: thesis: ( a in the carrier of X1 implies F . a = G . a )

hence
F . a = G . a
by A15, A16, XBOOLE_0:def 3; :: thesis: verumassume 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 = (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