let A, B be non empty set ; :: thesis: for A1, A2 being non empty Subset of A st A1 misses A2 holds

for f1 being Function of A1,B

for f2 being Function of A2,B holds

( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 )

let A1, A2 be non empty Subset of A; :: thesis: ( A1 misses A2 implies for f1 being Function of A1,B

for f2 being Function of A2,B holds

( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 ) )

assume A1: A1 misses A2 ; :: thesis: for f1 being Function of A1,B

for f2 being Function of A2,B holds

( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 )

let f1 be Function of A1,B; :: thesis: for f2 being Function of A2,B holds

( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 )

let f2 be Function of A2,B; :: thesis: ( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 )

A1 /\ A2 c= A2 by XBOOLE_1:17;

then reconsider g2 = f2 | (A1 /\ A2) as Function of {},B by A1, FUNCT_2:32;

A1 /\ A2 c= A1 by XBOOLE_1:17;

then reconsider g1 = f1 | (A1 /\ A2) as Function of {},B by A1, FUNCT_2:32;

g1 = g2 ;

hence ( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 ) by Def1; :: thesis: verum

for f1 being Function of A1,B

for f2 being Function of A2,B holds

( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 )

let A1, A2 be non empty Subset of A; :: thesis: ( A1 misses A2 implies for f1 being Function of A1,B

for f2 being Function of A2,B holds

( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 ) )

assume A1: A1 misses A2 ; :: thesis: for f1 being Function of A1,B

for f2 being Function of A2,B holds

( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 )

let f1 be Function of A1,B; :: thesis: for f2 being Function of A2,B holds

( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 )

let f2 be Function of A2,B; :: thesis: ( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 )

A1 /\ A2 c= A2 by XBOOLE_1:17;

then reconsider g2 = f2 | (A1 /\ A2) as Function of {},B by A1, FUNCT_2:32;

A1 /\ A2 c= A1 by XBOOLE_1:17;

then reconsider g1 = f1 | (A1 /\ A2) as Function of {},B by A1, FUNCT_2:32;

g1 = g2 ;

hence ( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 ) by Def1; :: thesis: verum