environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, TARSKI, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4, STRUCT_0, RCOMP_1, SETFAM_1, CONNSP_2, ORDINAL2, FUNCOP_1, FUNCT_3, ZFMISC_1, TSEP_1, CONNSP_1, TMAP_1, PARTFUN1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, DOMAIN_1, STRUCT_0, PRE_TOPC, CONNSP_1, CONNSP_2, BORSUK_1, TSEP_1;
definitions PRE_TOPC, BORSUK_1, XBOOLE_0;
theorems TARSKI, SUBSET_1, FUNCT_1, FUNCT_2, FUNCT_4, ZFMISC_1, PRE_TOPC, CONNSP_2, TOPS_2, BORSUK_1, TSEP_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, CONNSP_1;
schemes ;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, PRE_TOPC, BORSUK_1, TSEP_1, RELSET_1, PARTFUN1, TOPS_1;
constructors HIDDEN, SETFAM_1, FUNCT_4, CONNSP_1, BORSUK_1, TSEP_1, FUNCOP_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities XBOOLE_0, STRUCT_0, RELAT_1;
expansions PRE_TOPC, BORSUK_1, XBOOLE_0;
theorem
for
A,
B being non
empty set for
A1,
A2,
A3,
A12,
A23 being non
empty Subset of
A st
A12 = A1 \/ A2 &
A23 = A2 \/ A3 holds
for
f1 being
Function of
A1,
B for
f2 being
Function of
A2,
B for
f3 being
Function of
A3,
B st
f1 | (A1 /\ A2) = f2 | (A1 /\ A2) &
f2 | (A2 /\ A3) = f3 | (A2 /\ A3) &
f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds
for
f12 being
Function of
A12,
B for
f23 being
Function of
A23,
B st
f12 = f1 union f2 &
f23 = f2 union f3 holds
f12 union f3 = f1 union f23
Lm1:
for A being set holds {} is Function of A,{}