:: BORSUK_1 semantic presentation

theorem :: BORSUK_1:1
canceled;

theorem :: BORSUK_1:2
canceled;

theorem :: BORSUK_1:3
canceled;

theorem E1: :: BORSUK_1:4
for b1 being set
for b2 being Subset of b1 holds (id b1) " b2 = b2
proof
let c1 be set ;
let c2 be Subset of c1;
thus c2 = (id c1) " ((id c1) .: c2) by FUNCT_2:92
.= (id c1) " c2 by FUNCT_1:162 ;
end;

theorem E2: :: BORSUK_1:5
for b1, b2 being set
for b3 being Function holds
( b1 c= b3 " b2 implies b3 .: b1 c= b2 )
proof
let c1, c2 be set ;
let c3 be Function;
assume c1 c= c3 " c2 ;
then E3: c3 .: c1 c= c3 .: (c3 " c2) by RELAT_1:156;
c3 .: (c3 " c2) c= c2 by FUNCT_1:145;
hence c3 .: c1 c= c2 by E3, XBOOLE_1:1;
end;

theorem E3: :: BORSUK_1:6
for b1, b2, b3 being set holds (b1 --> b2) .: b3 c= {b2}
proof
let c1, c2, c3 be set ;
( (c1 --> c2) .: c3 c= rng (c1 --> c2) & rng (c1 --> c2) c= {c2} ) by FUNCOP_1:19, RELAT_1:144;
hence (c1 --> c2) .: c3 c= {c2} by XBOOLE_1:1;
end;

theorem :: BORSUK_1:7
canceled;

theorem :: BORSUK_1:8
canceled;

theorem E4: :: BORSUK_1:9
for b1, b2, b3 being set holds
( b1 c= [:b2,b3:] implies (.: (pr1 b2,b3)) . b1 = (pr1 b2,b3) .: b1 )
proof
let c1, c2, c3 be set ;
assume c1 c= [:c2,c3:] ;
then c1 c= dom (pr1 c2,c3) by FUNCT_3:def 5;
hence (.: (pr1 c2,c3)) . c1 = (pr1 c2,c3) .: c1 by FUNCT_3:def 1;
end;

theorem E5: :: BORSUK_1:10
for b1, b2, b3 being set holds
( b1 c= [:b2,b3:] implies (.: (pr2 b2,b3)) . b1 = (pr2 b2,b3) .: b1 )
proof
let c1, c2, c3 be set ;
assume c1 c= [:c2,c3:] ;
then c1 c= dom (pr2 c2,c3) by FUNCT_3:def 6;
hence (.: (pr2 c2,c3)) . c1 = (pr2 c2,c3) .: c1 by FUNCT_3:def 1;
end;

theorem :: BORSUK_1:11
canceled;

theorem E6: :: BORSUK_1:12
for b1, b2 being set
for b3 being Subset of b1
for b4 being Subset of b2 holds
( [:b3,b4:] <> {} implies ( (pr1 b1,b2) .: [:b3,b4:] = b3 & (pr2 b1,b2) .: [:b3,b4:] = b4 ) )
proof
let c1, c2 be set ;
let c3 be Subset of c1;
let c4 be Subset of c2;
assume [:c3,c4:] <> {} ;
then E7: ( c3 <> {} & c4 <> {} & c3 c= c1 & c4 c= c2 ) by ZFMISC_1:113;
then E8: ( c1 <> {} & c2 <> {} ) by XBOOLE_1:3;
now
let c5 be set ;
thus ( c5 in (pr1 c1,c2) .: [:c3,c4:] implies c5 in c3 )
proof
assume c5 in (pr1 c1,c2) .: [:c3,c4:] ;
then consider c6 being set such that
E9: ( c6 in [:c1,c2:] & c6 in [:c3,c4:] & c5 = (pr1 c1,c2) . c6 ) by FUNCT_2:115;
E10: c6 = [(c6 `1 ),(c6 `2 )] by E9, MCART_1:23;
E11: c6 `1 in c3 by E9, MCART_1:10;
( c6 `1 in c1 & c6 `2 in c2 ) by E9, MCART_1:10;
hence c5 in c3 by E9, E10, E11, FUNCT_3:def 5;
end;
consider c6 being Element of c4;
assume E9: c5 in c3 ;
then E10: ( c5 in c1 & c6 in c2 ) by E7, TARSKI:def 3;
E11: [c5,c6] in [:c3,c4:] by E7, E9, ZFMISC_1:106;
c5 = (pr1 c1,c2) . [c5,c6] by E10, FUNCT_3:def 5;
hence c5 in (pr1 c1,c2) .: [:c3,c4:] by E8, E11, FUNCT_2:43;
end;
hence (pr1 c1,c2) .: [:c3,c4:] = c3 by TARSKI:2;
now
let c5 be set ;
thus ( c5 in (pr2 c1,c2) .: [:c3,c4:] implies c5 in c4 )
proof
assume c5 in (pr2 c1,c2) .: [:c3,c4:] ;
then consider c6 being set such that
E9: ( c6 in [:c1,c2:] & c6 in [:c3,c4:] & c5 = (pr2 c1,c2) . c6 ) by FUNCT_2:115;
E10: c6 = [(c6 `1 ),(c6 `2 )] by E9, MCART_1:23;
E11: c6 `2 in c4 by E9, MCART_1:10;
( c6 `1 in c1 & c6 `2 in c2 ) by E9, MCART_1:10;
hence c5 in c4 by E9, E10, E11, FUNCT_3:def 6;
end;
consider c6 being Element of c3;
assume E9: c5 in c4 ;
then E10: ( c6 in c1 & c5 in c2 ) by E7, TARSKI:def 3;
E11: [c6,c5] in [:c3,c4:] by E7, E9, ZFMISC_1:106;
c5 = (pr2 c1,c2) . [c6,c5] by E10, FUNCT_3:def 6;
hence c5 in (pr2 c1,c2) .: [:c3,c4:] by E8, E11, FUNCT_2:43;
end;
hence (pr2 c1,c2) .: [:c3,c4:] = c4 by TARSKI:2;
end;

theorem E7: :: BORSUK_1:13
for b1, b2 being set
for b3 being Subset of b1
for b4 being Subset of b2 holds
( [:b3,b4:] <> {} implies ( (.: (pr1 b1,b2)) . [:b3,b4:] = b3 & (.: (pr2 b1,b2)) . [:b3,b4:] = b4 ) )
proof
let c1, c2 be set ;
let c3 be Subset of c1;
let c4 be Subset of c2;
assume E8: [:c3,c4:] <> {} ;
thus (.: (pr1 c1,c2)) . [:c3,c4:] = (pr1 c1,c2) .: [:c3,c4:] by E4
.= c3 by E8, E6 ;
thus (.: (pr2 c1,c2)) . [:c3,c4:] = (pr2 c1,c2) .: [:c3,c4:] by E5
.= c4 by E8, E6 ;
end;

theorem E8: :: BORSUK_1:14
for b1, b2 being set
for b3 being Subset of [:b1,b2:]
for b4 being Subset-Family of [:b1,b2:] holds
( for b5 being set holds
( b5 in b4 implies ( b5 c= b3 & ex b6 being Subset of b1ex b7 being Subset of b2 st b5 = [:b6,b7:] ) ) implies [:(union ((.: (pr1 b1,b2)) .: b4)),(meet ((.: (pr2 b1,b2)) .: b4)):] c= b3 )
proof
let c1, c2 be set ;
let c3 be Subset of [:c1,c2:];
let c4 be Subset-Family of [:c1,c2:];
assume E9: for b1 being set holds
( b1 in c4 implies ( b1 c= c3 & ex b2 being Subset of c1ex b3 being Subset of c2 st b1 = [:b2,b3:] ) ) ;
let c5 be set ; :: uses TARSKI:def 3
assume E10: c5 in [:(union ((.: (pr1 c1,c2)) .: c4)),(meet ((.: (pr2 c1,c2)) .: c4)):] ;
then E11: ( c5 `1 in union ((.: (pr1 c1,c2)) .: c4) & c5 `2 in meet ((.: (pr2 c1,c2)) .: c4) ) by MCART_1:10;
then consider c6 being set such that
E12: ( c5 `1 in c6 & c6 in (.: (pr1 c1,c2)) .: c4 ) by TARSKI:def 4;
consider c7 being set such that
E13: ( c7 in dom (.: (pr1 c1,c2)) & c7 in c4 & c6 = (.: (pr1 c1,c2)) . c7 ) by E12, FUNCT_1:def 12;
consider c8 being Subset of c1, c9 being Subset of c2 such that
E14: c7 = [:c8,c9:] by E9, E13;
E15: c7 <> {} by E12, E13, FUNCT_3:9;
c7 in bool [:c1,c2:] by E13;
then c7 in bool (dom (pr2 c1,c2)) by FUNCT_3:def 6;
then c7 in dom (.: (pr2 c1,c2)) by FUNCT_3:def 1;
then (.: (pr2 c1,c2)) . c7 in (.: (pr2 c1,c2)) .: c4 by E13, FUNCT_1:def 12;
then c9 in (.: (pr2 c1,c2)) .: c4 by E14, E15, E7;
then E16: ( c5 `1 in c8 & c5 `2 in c9 ) by E11, E12, E13, E14, E15, E7, SETFAM_1:def 1;
ex b1, b2 being set st c5 = [b1,b2] by E10, ZFMISC_1:102;
then E17: c5 in c7 by E14, E16, MCART_1:11;
c7 c= c3 by E9, E13;
hence c5 in c3 by E17;
end;

theorem :: BORSUK_1:15
for b1, b2 being set
for b3 being Subset of [:b1,b2:]
for b4 being Subset-Family of [:b1,b2:] holds
( for b5 being set holds
( b5 in b4 implies ( b5 c= b3 & ex b6 being Subset of b1ex b7 being Subset of b2 st b5 = [:b6,b7:] ) ) implies [:(meet ((.: (pr1 b1,b2)) .: b4)),(union ((.: (pr2 b1,b2)) .: b4)):] c= b3 )
proof
let c1, c2 be set ;
let c3 be Subset of [:c1,c2:];
let c4 be Subset-Family of [:c1,c2:];
assume E9: for b1 being set holds
( b1 in c4 implies ( b1 c= c3 & ex b2 being Subset of c1ex b3 being Subset of c2 st b1 = [:b2,b3:] ) ) ;
let c5 be set ; :: uses TARSKI:def 3
assume E10: c5 in [:(meet ((.: (pr1 c1,c2)) .: c4)),(union ((.: (pr2 c1,c2)) .: c4)):] ;
then E11: ( c5 `1 in meet ((.: (pr1 c1,c2)) .: c4) & c5 `2 in union ((.: (pr2 c1,c2)) .: c4) ) by MCART_1:10;
then consider c6 being set such that
E12: ( c5 `2 in c6 & c6 in (.: (pr2 c1,c2)) .: c4 ) by TARSKI:def 4;
consider c7 being set such that
E13: ( c7 in dom (.: (pr2 c1,c2)) & c7 in c4 & c6 = (.: (pr2 c1,c2)) . c7 ) by E12, FUNCT_1:def 12;
consider c8 being Subset of c1, c9 being Subset of c2 such that
E14: c7 = [:c8,c9:] by E9, E13;
E15: c7 <> {} by E12, E13, FUNCT_3:9;
c7 in bool [:c1,c2:] by E13;
then c7 in bool (dom (pr1 c1,c2)) by FUNCT_3:def 5;
then c7 in dom (.: (pr1 c1,c2)) by FUNCT_3:def 1;
then (.: (pr1 c1,c2)) . c7 in (.: (pr1 c1,c2)) .: c4 by E13, FUNCT_1:def 12;
then c8 in (.: (pr1 c1,c2)) .: c4 by E14, E15, E7;
then E16: ( c5 `1 in c8 & c5 `2 in c9 ) by E11, E12, E13, E14, E15, E7, SETFAM_1:def 1;
ex b1, b2 being set st c5 = [b1,b2] by E10, ZFMISC_1:102;
then E17: c5 in c7 by E14, E16, MCART_1:11;
c7 c= c3 by E9, E13;
hence c5 in c3 by E17;
end;

theorem E9: :: BORSUK_1:16
for b1 being set
for b2 being non empty set
for b3 being Function of b1,b2
for b4 being Subset-Family of b1 holds union ((.: b3) .: b4) = b3 .: (union b4)
proof
let c1 be set ;
let c2 be non empty set ;
let c3 be Function of c1,c2;
let c4 be Subset-Family of c1;
dom c3 = c1 by FUNCT_2:def 1;
hence union ((.: c3) .: c4) = c3 .: (union c4) by FUNCT_3:16;
end;

theorem E10: :: BORSUK_1:17
for b1 being set
for b2 being Subset-Family of b1 holds union (union b2) = union { (union b3) where B is Subset of b1 : b3 in b2 }
proof
let c1 be set ;
let c2 be Subset-Family of c1;
thus union (union c2) c= union { (union b1) where B is Subset of c1 : b1 in c2 } :: uses XBOOLE_0:def 10
proof
let c3 be set ; :: uses TARSKI:def 3
assume c3 in union (union c2) ;
then consider c4 being set such that
E11: ( c3 in c4 & c4 in union c2 ) by TARSKI:def 4;
consider c5 being set such that
E12: ( c4 in c5 & c5 in c2 ) by E11, TARSKI:def 4;
E13: c3 in union c5 by E11, E12, TARSKI:def 4;
union c5 in { (union b1) where B is Subset of c1 : b1 in c2 } by E12;
hence c3 in union { (union b1) where B is Subset of c1 : b1 in c2 } by E13, TARSKI:def 4;
end;
let c3 be set ; :: uses TARSKI:def 3
assume c3 in union { (union b1) where B is Subset of c1 : b1 in c2 } ;
then consider c4 being set such that
E11: ( c3 in c4 & c4 in { (union b1) where B is Subset of c1 : b1 in c2 } ) by TARSKI:def 4;
consider c5 being Subset of c1 such that
E12: ( c4 = union c5 & c5 in c2 ) by E11;
consider c6 being set such that
E13: ( c3 in c6 & c6 in c5 ) by E11, E12, TARSKI:def 4;
c6 in union c2 by E12, E13, TARSKI:def 4;
hence c3 in union (union c2) by E13, TARSKI:def 4;
end;

theorem E11: :: BORSUK_1:18
for b1 being set
for b2 being Subset-Family of b1 holds
( union b2 = b1 implies for b3 being Subset of b2
for b4 being Subset of b1 holds
( b4 = union b3 implies b4 ` c= union (b3 ` ) ) )
proof
let c1 be set ;
let c2 be Subset-Family of c1;
assume E12: union c2 = c1 ;
let c3 be Subset of c2;
let c4 be Subset of c1;
assume E13: c4 = union c3 ;
let c5 be set ; :: uses TARSKI:def 3
assume E14: c5 in c4 ` ;
then consider c6 being set such that
E15: ( c5 in c6 & c6 in c2 ) by E12, TARSKI:def 4;
not c5 in c4 by E14, SUBSET_1:54;
then not c6 in c3 by E13, E15, TARSKI:def 4;
then c6 in c3 ` by E15, SUBSET_1:50;
hence c5 in union (c3 ` ) by E15, TARSKI:def 4;
end;

theorem E12: :: BORSUK_1:19
for b1, b2, b3 being non empty set
for b4 being Function of b1,b2
for b5 being Function of b1,b3 holds
not ( for b6, b7 being Element of b1 holds
( b4 . b6 = b4 . b7 implies b5 . b6 = b5 . b7 ) & for b6 being Function of b2,b3 holds
not b6 * b4 = b5 )
proof
let c1, c2, c3 be non empty set ;
let c4 be Function of c1,c2;
let c5 be Function of c1,c3;
assume E13: for b1, b2 being Element of c1 holds
( c4 . b1 = c4 . b2 implies c5 . b1 = c5 . b2 ) ;
defpred S1[ set , set ] means ( for b1 being Element of c1 holds
not a1 = c4 . b1 or for b1 being Element of c1 holds
( a1 = c4 . b1 implies a2 = c5 . b1 ) );
E14: now
let c6 be set ;
assume c6 in c2 ;
now
per cases not ( for b1 being Element of c1 holds
not c6 = c4 . b1 & ex b1 being Element of c1 st c6 = c4 . b1 ) ;
case ex b1 being Element of c1 st c6 = c4 . b1 ;
then consider c7 being Element of c1 such that
E15: c6 = c4 . c7 ;
take c8 = c5 . c7;
thus ( c8 in c3 & not ( ex b1 being Element of c1 st c6 = c4 . b1 & for b1 being Element of c1 holds
not ( c6 = c4 . b1 & c8 = c5 . b1 ) ) ) by E15;
end;
case E15: for b1 being Element of c1 holds
not c6 = c4 . b1 ;
consider c7 being Element of c3;
c7 in c3 ;
hence ex b1 being set st
( b1 in c3 & not ( ex b2 being Element of c1 st c6 = c4 . b2 & for b2 being Element of c1 holds
not ( c6 = c4 . b2 & b1 = c5 . b2 ) ) ) by E15;
end;
end;
end;
then consider c7 being set such that
E15: c7 in c3
and E16: not ( ex b1 being Element of c1 st c6 = c4 . b1 & for b1 being Element of c1 holds
not ( c6 = c4 . b1 & c7 = c5 . b1 ) ) ;
take c8 = c7;
thus c8 in c3 by E15;
thus S1[c6,c8] by E13, E16;
end;
consider c6 being Function of c2,c3 such that
E15: for b1 being set holds
( b1 in c2 implies S1[b1,c6 . b1] ) from FUNCT_2:sch 1(E14);
 take c6 ;
now
let c7 be Element of c1;
thus (c6 * c4) . c7 = c6 . (c4 . c7) by FUNCT_2:21
.= c5 . c7 by E15 ;
end;
hence c6 * c4 = c5 by FUNCT_2:113;
end;

theorem E13: :: BORSUK_1:20
for b1, b2, b3 being non empty set
for b4 being Element of b2
for b5 being Function of b1,b2
for b6 being Function of b2,b3 holds b5 " {b4} c= (b6 * b5) " {(b6 . b4)}
proof
let c1, c2, c3 be non empty set ;
let c4 be Element of c2;
let c5 be Function of c1,c2;
let c6 be Function of c2,c3;
c5 " {c4} c= (c6 * c5) " (c6 .: {c4}) by FUNCT_2:53;
hence c5 " {c4} c= (c6 * c5) " {(c6 . c4)} by SETWISEO:13;
end;

theorem E14: :: BORSUK_1:21
for b1, b2, b3 being non empty set
for b4 being Function of b1,b2
for b5 being Element of b1
for b6 being Element of b3 holds [:b4,(id b3):] . [b5,b6] = [(b4 . b5),b6]
proof
let c1, c2, c3 be non empty set ;
let c4 be Function of c1,c2;
let c5 be Element of c1;
let c6 be Element of c3;
thus [:c4,(id c3):] . [c5,c6] = [(c4 . c5),((id c3) . c6)] by FUNCT_3:96
.= [(c4 . c5),c6] by FUNCT_1:35 ;
end;

theorem :: BORSUK_1:22
canceled;

theorem E15: :: BORSUK_1:23
for b1, b2, b3 being non empty set
for b4 being Function of b1,b2
for b5 being Subset of b1
for b6 being Subset of b3 holds [:b4,(id b3):] .: [:b5,b6:] = [:(b4 .: b5),b6:]
proof
let c1, c2, c3 be non empty set ;
let c4 be Function of c1,c2;
let c5 be Subset of c1;
let c6 be Subset of c3;
thus [:c4,(id c3):] .: [:c5,c6:] = [:(c4 .: c5),((id c3) .: c6):] by FUNCT_3:93
.= [:(c4 .: c5),c6:] by FUNCT_1:162 ;
end;

theorem E16: :: BORSUK_1:24
for b1, b2, b3 being non empty set
for b4 being Function of b1,b2
for b5 being Element of b2
for b6 being Element of b3 holds [:b4,(id b3):] " {[b5,b6]} = [:(b4 " {b5}),{b6}:]
proof
let c1, c2, c3 be non empty set ;
let c4 be Function of c1,c2;
let c5 be Element of c2;
let c6 be Element of c3;
thus [:c4,(id c3):] " {[c5,c6]} = [:c4,(id c3):] " [:{c5},{c6}:] by ZFMISC_1:35
.= [:(c4 " {c5}),((id c3) " {c6}):] by FUNCT_3:94
.= [:(c4 " {c5}),{c6}:] by E1 ;
end;

definition
let c1 be non empty set ;
let c2 be set ;
let c3 be Element of c1;
redefine func --> as a2 --> a3 -> Function of a2,a1;
coherence
c2 --> c3 is Function of c2,c1 by FUNCOP_1:58;
end;

theorem E17: :: BORSUK_1:25
for b1 being non empty set
for b2 being Subset-Family of b1
for b3 being Subset of b2 holds
union b3 is Subset of b1
proof
let c1 be non empty set ;
let c2 be Subset-Family of c1;
let c3 be Subset of c2;
union c3 c= c1
proof
let c4 be set ; :: uses TARSKI:def 3
assume c4 in union c3 ;
then consider c5 being set such that
E18: ( c4 in c5 & c5 in c3 ) by TARSKI:def 4;
c4 in union c2 by E18, TARSKI:def 4;
hence c4 in c1 ;
end;
hence union c3 is Subset of c1 ;
end;

theorem E18: :: BORSUK_1:26
for b1 being set
for b2 being a_partition of b1
for b3, b4 being Subset of b2 holds union (b3 /\ b4) = (union b3) /\ (union b4)
proof
let c1 be set ;
let c2 be a_partition of c1;
let c3, c4 be Subset of c2;
thus union (c3 /\ c4) c= (union c3) /\ (union c4) by ZFMISC_1:97; :: uses XBOOLE_0:def 10
let c5 be set ; :: uses TARSKI:def 3
assume E19: c5 in (union c3) /\ (union c4) ;
then c5 in union c3 by XBOOLE_0:def 3;
then consider c6 being set such that
E20: ( c5 in c6 & c6 in c3 ) by TARSKI:def 4;
c5 in union c4 by E19, XBOOLE_0:def 3;
then consider c7 being set such that
E21: ( c5 in c7 & c7 in c4 ) by TARSKI:def 4;
E22: ( c6 in c2 & c7 in c2 ) by E20, E21;
not c6 misses c7 by E20, E21, XBOOLE_0:3;
then c6 = c7 by E20, E22, EQREL_1:def 6;
then c6 in c3 /\ c4 by E20, E21, XBOOLE_0:def 3;
hence c5 in union (c3 /\ c4) by E20, TARSKI:def 4;
end;

theorem E19: :: BORSUK_1:27
for b1 being non empty set
for b2 being a_partition of b1
for b3 being Subset of b2
for b4 being Subset of b1 holds
( b4 = union b3 implies b4 ` = union (b3 ` ) )
proof
let c1 be non empty set ;
let c2 be a_partition of c1;
let c3 be Subset of c2;
let c4 be Subset of c1;
assume E20: c4 = union c3 ;
union c2 = c1 by EQREL_1:def 6;
hence c4 ` c= union (c3 ` ) by E20, E11; :: uses XBOOLE_0:def 10
let c5 be set ; :: uses TARSKI:def 3
assume c5 in union (c3 ` ) ;
then consider c6 being set such that
E21: ( c5 in c6 & c6 in c3 ` ) by TARSKI:def 4;
E22: c6 in c2 by E21;
assume not c5 in c4 ` ;
then c5 in c4 by E21, E22, SUBSET_1:50;
then consider c7 being set such that
E23: ( c5 in c7 & c7 in c3 ) by E20, TARSKI:def 4;
E24: c7 in c2 by E23;
not c6 misses c7 by E21, E23, XBOOLE_0:3;
then c6 = c7 by E22, E24, EQREL_1:def 6;
hence not verum by E21, E23, SUBSET_1:54;
end;

theorem :: BORSUK_1:28
for b1 being non empty set
for b2 being Equivalence_Relation of b1 holds
not Class b2 is empty ;

registration
let c1 be non empty set ;
cluster non empty a_partition of a1;
existence
not for b1 being a_partition of c1 holds b1 is empty
proof
reconsider c2 = Class (nabla c1) as a_partition of c1 ;
take c2 ;
consider c3 being Element of c1;
thus not c2 is empty ;
end;
end;

definition
let c1 be non empty set ;
let c2 be non empty a_partition of c1;
func proj a2 -> Function of a1,a2 means :E20: :: BORSUK_1:def 1
for b1 being Element of a1 holds b1 in a3 . b1;
existence
ex b1 being Function of c1,c2 st
for b2 being Element of c1 holds b2 in b1 . b2
proof
defpred S1[ set , set ] means a1 in a2;
E20: now
let c3 be set ;
assume E21: c3 in c1 ;
union c2 = c1 by EQREL_1:def 6;
then ex b1 being set st
( c3 in b1 & b1 in c2 ) by E21, TARSKI:def 4;
hence ex b1 being set st
( b1 in c2 & S1[c3,b1] ) ;
end;
consider c3 being Function of c1,c2 such that
E21: for b1 being set holds
( b1 in c1 implies S1[b1,c3 . b1] ) from FUNCT_2:sch 1(E20);
 take c3 ;
let c4 be Element of c1;
thus c4 in c3 . c4 by E21;
end;
correctness
uniqueness
for b1, b2 being Function of c1,c2 holds
( ( for b3 being Element of c1 holds b3 in b1 . b3 & for b3 being Element of c1 holds b3 in b2 . b3 ) implies ( b1 = b2 ) );
proof
let c3, c4 be Function of c1,c2;
assume that E20: for b1 being Element of c1 holds b1 in c3 . b1
and E21: for b1 being Element of c1 holds b1 in c4 . b1 ;
now
let c5 be Element of c1;
E22: ( c3 . c5 is Subset of c1 & c4 . c5 is Subset of c1 ) by TARSKI:def 3;
( c5 in c3 . c5 & c5 in c4 . c5 ) by E20, E21;
then not c3 . c5 misses c4 . c5 by XBOOLE_0:3;
hence c3 . c5 = c4 . c5 by E22, EQREL_1:def 6;
end;
hence c3 = c4 by FUNCT_2:113;
end;
end;

:: deftheorem E20 defines proj BORSUK_1:def 1 :
for b1 being non empty set
for b2 being non empty a_partition of b1
for b3 being Function of b1,b2 holds
( b3 = proj b2 iff for b4 being Element of b1 holds b4 in b3 . b4 );

theorem E21: :: BORSUK_1:29
for b1 being non empty set
for b2 being non empty a_partition of b1
for b3 being Element of b1
for b4 being Element of b2 holds
( b3 in b4 implies b4 = (proj b2) . b3 )
proof
let c1 be non empty set ;
let c2 be non empty a_partition of c1;
let c3 be Element of c1;
let c4 be Element of c2;
assume E22: c3 in c4 ;
E23: (proj c2) . c3 is Subset of c1 by TARSKI:def 3;
c3 in (proj c2) . c3 by E20;
then not (proj c2) . c3 misses c4 by E22, XBOOLE_0:3;
hence c4 = (proj c2) . c3 by E23, EQREL_1:def 6;
end;

theorem E22: :: BORSUK_1:30
for b1 being non empty set
for b2 being non empty a_partition of b1
for b3 being Element of b2 holds b3 = (proj b2) " {b3}
proof
let c1 be non empty set ;
let c2 be non empty a_partition of c1;
let c3 be Element of c2;
thus c3 c= (proj c2) " {c3} :: uses XBOOLE_0:def 10
proof
let c4 be set ; :: uses TARSKI:def 3
assume E23: c4 in c3 ;
then (proj c2) . c4 = c3 by E21;
then (proj c2) . c4 in {c3} by TARSKI:def 1;
hence c4 in (proj c2) " {c3} by E23, FUNCT_2:46;
end;
let c4 be set ; :: uses TARSKI:def 3
assume E23: c4 in (proj c2) " {c3} ;
then (proj c2) . c4 in {c3} by FUNCT_1:def 13;
then (proj c2) . c4 = c3 by TARSKI:def 1;
hence c4 in c3 by E23, E20;
end;

theorem E23: :: BORSUK_1:31
for b1 being non empty set
for b2 being non empty a_partition of b1
for b3 being Subset of b2 holds (proj b2) " b3 = union b3
proof
let c1 be non empty set ;
let c2 be non empty a_partition of c1;
let c3 be Subset of c2;
thus (proj c2) " c3 c= union c3 :: uses XBOOLE_0:def 10
proof
let c4 be set ; :: uses TARSKI:def 3
assume E24: c4 in (proj c2) " c3 ;
then E25: (proj c2) . c4 in c3 by FUNCT_2:46;
c4 in (proj c2) . c4 by E24, E20;
hence c4 in union c3 by E25, TARSKI:def 4;
end;
let c4 be set ; :: uses TARSKI:def 3
assume c4 in union c3 ;
then consider c5 being set such that
E24: ( c4 in c5 & c5 in c3 ) by TARSKI:def 4;
E25: c5 in c2 by E24;
then (proj c2) . c4 = c5 by E24, E21;
hence c4 in (proj c2) " c3 by E24, E25, FUNCT_2:46;
end;

theorem E24: :: BORSUK_1:32
for b1 being non empty set
for b2 being non empty a_partition of b1
for b3 being Element of b2 holds
ex b4 being Element of b1 st (proj b2) . b4 = b3
proof
let c1 be non empty set ;
let c2 be non empty a_partition of c1;
let c3 be Element of c2;
reconsider c4 = c3 as Subset of c1 ;
c4 <> {} by EQREL_1:def 6;
then consider c5 being Element of c1 such that
E25: c5 in c4 by SUBSET_1:10;
take c5 ;
thus (proj c2) . c5 = c3 by E25, E21;
end;

theorem E25: :: BORSUK_1:33
for b1 being non empty set
for b2 being non empty a_partition of b1
for b3 being Subset of b1 holds
( for b4 being Subset of b1 holds
( ( b4 in b2 ) implies ( not b4 meets b3 or b4 c= b3 ) ) implies b3 = (proj b2) " ((proj b2) .: b3) )
proof
let c1 be non empty set ;
let c2 be non empty a_partition of c1;
let c3 be Subset of c1;
assume E26: for b1 being Subset of c1 holds
( ( b1 in c2 ) implies ( not b1 meets c3 or b1 c= c3 ) ) ;
c3 c= c1 ;
then c3 c= dom (proj c2) by FUNCT_2:def 1;
hence c3 c= (proj c2) " ((proj c2) .: c3) by FUNCT_1:146; :: uses XBOOLE_0:def 10
let c4 be set ; :: uses TARSKI:def 3
assume E27: c4 in (proj c2) " ((proj c2) .: c3) ;
then reconsider c5 = c4 as Element of c1 ;
(proj c2) . c4 in (proj c2) .: c3 by E27, FUNCT_1:def 13;
then consider c6 being Element of c1 such that
E28: ( c6 in c3 & (proj c2) . c5 = (proj c2) . c6 ) by FUNCT_2:116;
reconsider c7 = (proj c2) . c6 as Subset of c1 by TARSKI:def 3;
c6 in (proj c2) . c6 by E20;
then c7 meets c3 by E28, XBOOLE_0:3;
then E29: c7 c= c3 by E26;
c5 in c7 by E28, E20;
hence c4 in c3 by E29;
end;

theorem :: BORSUK_1:34
canceled;

theorem E26: :: BORSUK_1:35
for b1 being TopStruct
for b2 being SubSpace of b1 holds the carrier of b2 c= the carrier of b1
proof
let c1 be TopStruct ;
let c2 be SubSpace of c1;
( the carrier of c2 = [#] c2 & the carrier of c1 = [#] c1 ) ;
hence the carrier of c2 c= the carrier of c1 by PRE_TOPC:def 9;
end;

definition
let c1, c2 be non empty TopSpace;
let c3 be Function of c1,c2;
means :: BORSUK_1:def 2
for b1 being Point of a1
for b2 being a_neighborhood of a3 . b1 holds
ex b3 being a_neighborhood of b1 st a3 .: b3 c= b2;
compatibility
( c3 is continuous iff for b1 being Point of c1
for b2 being a_neighborhood of c3 . b1 holds
ex b3 being a_neighborhood of b1 st c3 .: b3 c= b2 )
proof
thus ( c3 is continuous implies for b1 being Point of c1
for b2 being a_neighborhood of c3 . b1 holds
ex b3 being a_neighborhood of b1 st c3 .: b3 c= b2 )
proof
assume E27: c3 is continuous ;
let c4 be Point of c1;
let c5 be a_neighborhood of c3 . c4;
c3 . c4 in Int c5 by CONNSP_2:def 1;
then E28: c4 in c3 " (Int c5) by FUNCT_2:46;
Int c5 is open by TOPS_1:51;
then c3 " (Int c5) is open by E27, TOPS_2:55;
then c4 in Int (c3 " (Int c5)) by E28, TOPS_1:55;
then reconsider c6 = c3 " (Int c5) as a_neighborhood of c4 by CONNSP_2:def 1;
take c6 ;
Int c5 c= c5 by TOPS_1:44;
then c6 c= c3 " c5 by RELAT_1:178;
hence c3 .: c6 c= c5 by E2;
end;
assume E27: for b1 being Point of c1
for b2 being a_neighborhood of c3 . b1 holds
ex b3 being a_neighborhood of b1 st c3 .: b3 c= b2 ;
now
let c4 be Subset of c2;
assume E28: c4 is open ;
now
let c5 be set ;
thus not ( c5 in c3 " c4 & for b1 being Subset of c1 holds
not ( b1 is open & b1 c= c3 " c4 & c5 in b1 ) )
proof
assume E29: c5 in c3 " c4 ;
then reconsider c6 = c5 as Point of c1 ;
E30: c3 . c6 in c4 by E29, FUNCT_2:46;
Int c4 = c4 by E28, TOPS_1:55;
then c4 is a_neighborhood of c3 . c6 by E30, CONNSP_2:def 1;
then c