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) )
proof
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;
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;
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