set B = the carrier of Y;

set A = the carrier of (X1 union X2);

set A2 = the carrier of X2;

set A1 = the carrier of X1;

A2: ( X1 is SubSpace of X1 union X2 & X2 is SubSpace of X1 union X2 ) by TSEP_1:22;

A3: the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def 2;

A4: ( the carrier of X1 meets the carrier of X2 implies f1 | ( the carrier of X1 /\ the carrier of X2) = f2 | ( the carrier of X1 /\ the carrier of X2) )

reconsider g1 = f1 as Function of A1, the carrier of Y ;

reconsider g2 = f2 as Function of A2, the carrier of Y ;

set G = g1 union g2;

the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def 2;

then reconsider F = g1 union g2 as Function of (X1 union X2),Y ;

take F ; :: thesis: ( F | X1 = f1 & F | X2 = f2 )

( (g1 union g2) | A1 = f1 & (g1 union g2) | A2 = f2 ) by A4, Def1, Th1;

hence ( F | X1 = f1 & F | X2 = f2 ) by A2, Def5; :: thesis: verum

set A = the carrier of (X1 union X2);

set A2 = the carrier of X2;

set A1 = the carrier of X1;

A2: ( X1 is SubSpace of X1 union X2 & X2 is SubSpace of X1 union X2 ) by TSEP_1:22;

A3: the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def 2;

A4: ( the carrier of X1 meets the carrier of X2 implies f1 | ( the carrier of X1 /\ the carrier of X2) = f2 | ( the carrier of X1 /\ the carrier of X2) )

proof

reconsider A1 = the carrier of X1, A2 = the carrier of X2 as non empty Subset of the carrier of (X1 union X2) by A3, XBOOLE_1:7;
assume A5:
the carrier of X1 meets the carrier of X2
; :: thesis: f1 | ( the carrier of X1 /\ the carrier of X2) = f2 | ( the carrier of X1 /\ the carrier of X2)

then A6: X1 meets X2 by TSEP_1:def 3;

then A7: X1 meet X2 is SubSpace of X1 by TSEP_1:27;

A8: X1 meet X2 is SubSpace of X2 by A6, TSEP_1:27;

thus f1 | ( the carrier of X1 /\ the carrier of X2) = f1 | the carrier of (X1 meet X2) by A6, TSEP_1:def 4

.= f2 | (X1 meet X2) by A1, A5, A7, Def5, TSEP_1:def 3

.= f2 | the carrier of (X1 meet X2) by A8, Def5

.= f2 | ( the carrier of X1 /\ the carrier of X2) by A6, TSEP_1:def 4 ; :: thesis: verum

end;then A6: X1 meets X2 by TSEP_1:def 3;

then A7: X1 meet X2 is SubSpace of X1 by TSEP_1:27;

A8: X1 meet X2 is SubSpace of X2 by A6, TSEP_1:27;

thus f1 | ( the carrier of X1 /\ the carrier of X2) = f1 | the carrier of (X1 meet X2) by A6, TSEP_1:def 4

.= f2 | (X1 meet X2) by A1, A5, A7, Def5, TSEP_1:def 3

.= f2 | the carrier of (X1 meet X2) by A8, Def5

.= f2 | ( the carrier of X1 /\ the carrier of X2) by A6, TSEP_1:def 4 ; :: thesis: verum

reconsider g1 = f1 as Function of A1, the carrier of Y ;

reconsider g2 = f2 as Function of A2, the carrier of Y ;

set G = g1 union g2;

the carrier of (X1 union X2) = the carrier of X1 \/ the carrier of X2 by TSEP_1:def 2;

then reconsider F = g1 union g2 as Function of (X1 union X2),Y ;

take F ; :: thesis: ( F | X1 = f1 & F | X2 = f2 )

( (g1 union g2) | A1 = f1 & (g1 union g2) | A2 = f2 ) by A4, Def1, Th1;

hence ( F | X1 = f1 & F | X2 = f2 ) by A2, Def5; :: thesis: verum