let X, Y be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
for f1 being Function of X1,Y
for f2 being Function of X2,Y holds
( ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) iff f1 | (X1 meet X2) = f2 | (X1 meet X2) )
let X1, X2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 implies for f1 being Function of X1,Y
for f2 being Function of X2,Y holds
( ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) iff f1 | (X1 meet X2) = f2 | (X1 meet X2) ) )
assume A1: X1 meets X2 ; :: thesis: for f1 being Function of X1,Y
for f2 being Function of X2,Y holds
( ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) iff f1 | (X1 meet X2) = f2 | (X1 meet X2) )
let f1 be Function of X1,Y; :: thesis: for f2 being Function of X2,Y holds
( ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) iff f1 | (X1 meet X2) = f2 | (X1 meet X2) )
let f2 be Function of X2,Y; :: thesis: ( ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) iff f1 | (X1 meet X2) = f2 | (X1 meet X2) )
thus ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 implies f1 | (X1 meet X2) = f2 | (X1 meet X2) ) :: thesis: ( f1 | (X1 meet X2) = f2 | (X1 meet X2) implies ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) )
proof
A2: ( X1 meet X2 is SubSpace of X2 & X2 is SubSpace of X1 union X2 ) by A1, TSEP_1:22, TSEP_1:27;
assume that
A3: (f1 union f2) | X1 = f1 and
A4: (f1 union f2) | X2 = f2 ; :: thesis: f1 | (X1 meet X2) = f2 | (X1 meet X2)
( X1 meet X2 is SubSpace of X1 & X1 is SubSpace of X1 union X2 ) by A1, TSEP_1:22, TSEP_1:27;
then (f1 union f2) | (X1 meet X2) = f1 | (X1 meet X2) by A3, Th72;
hence f1 | (X1 meet X2) = f2 | (X1 meet X2) by A2, A4, Th72; :: thesis: verum
end;
thus ( f1 | (X1 meet X2) = f2 | (X1 meet X2) implies ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) ) by Def12; :: thesis: verum