:: 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 :: 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 E3: :: 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 E4: :: 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 E5: :: 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 E6: ( c3 <> {} & c4 <> {} & c3 c= c1 & c4 c= c2 ) by ZFMISC_1:113;
then E7: ( 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
E8: ( c6 in [:c1,c2:] & c6 in [:c3,c4:] & c5 = (pr1 c1,c2) . c6 ) by FUNCT_2:115;
E9: c6 = [(c6 `1 ),(c6 `2 )] by E8, MCART_1:23;
E10: c6 `1 in c3 by E8, MCART_1:10;
( c6 `1 in c1 & c6 `2 in c2 ) by E8, MCART_1:10;
hence c5 in c3 by E8, E9, E10, FUNCT_3:def 5;
end;
consider c6 being Element of c4;
assume E8: c5 in c3 ;
then E9: ( c5 in c1 & c6 in c2 ) by E6, TARSKI:def 3;
E10: [c5,c6] in [:c3,c4:] by E6, E8, ZFMISC_1:106;
c5 = (pr1 c1,c2) . [c5,c6] by E9, FUNCT_3:def 5;
hence c5 in (pr1 c1,c2) .: [:c3,c4:] by E7, E10, 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
E8: ( c6 in [:c1,c2:] & c6 in [:c3,c4:] & c5 = (pr2 c1,c2) . c6 ) by FUNCT_2:115;
E9: c6 = [(c6 `1 ),(c6 `2 )] by E8, MCART_1:23;
E10: c6 `2 in c4 by E8, MCART_1:10;
( c6 `1 in c1 & c6 `2 in c2 ) by E8, MCART_1:10;
hence c5 in c4 by E8, E9, E10, FUNCT_3:def 6;
end;
consider c6 being Element of c3;
assume E8: c5 in c4 ;
then E9: ( c6 in c1 & c5 in c2 ) by E6, TARSKI:def 3;
E10: [c6,c5] in [:c3,c4:] by E6, E8, ZFMISC_1:106;
c5 = (pr2 c1,c2) . [c6,c5] by E9, FUNCT_3:def 6;
hence c5 in (pr2 c1,c2) .: [:c3,c4:] by E7, E10, FUNCT_2:43;
end;
hence (pr2 c1,c2) .: [:c3,c4:] = c4 by TARSKI:2;
end;

theorem E6: :: 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 E7: [:c3,c4:] <> {} ;
thus (.: (pr1 c1,c2)) . [:c3,c4:] = (pr1 c1,c2) .: [:c3,c4:] by E3
.= c3 by E7, E5 ;
thus (.: (pr2 c1,c2)) . [:c3,c4:] = (pr2 c1,c2) .: [:c3,c4:] by E4
.= c4 by E7, E5 ;
end;

theorem E7: :: 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 E8: 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 ; :: according to TARSKI:def 3
assume E9: c5 in [:(union ((.: (pr1 c1,c2)) .: c4)),(meet ((.: (pr2 c1,c2)) .: c4)):] ;
then E10: ( 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
E11: ( c5 `1 in c6 & c6 in (.: (pr1 c1,c2)) .: c4 ) by TARSKI:def 4;
consider c7 being set such that
E12: ( c7 in dom (.: (pr1 c1,c2)) & c7 in c4 & c6 = (.: (pr1 c1,c2)) . c7 ) by E11, FUNCT_1:def 12;
consider c8 being Subset of c1, c9 being Subset of c2 such that
E13: c7 = [:c8,c9:] by E8, E12;
E14: c7 <> {} by E11, E12, FUNCT_3:9;
c7 in bool [:c1,c2:] by E12;
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 E12, FUNCT_1:def 12;
then c9 in (.: (pr2 c1,c2)) .: c4 by E13, E14, E6;
then E15: ( c5 `1 in c8 & c5 `2 in c9 ) by E10, E11, E12, E13, E14, E6, SETFAM_1:def 1;
ex b1, b2 being set st c5 = [b1,b2] by E9, ZFMISC_1:102;
then E16: c5 in c7 by E13, E15, MCART_1:11;
c7 c= c3 by E8, E12;
hence c5 in c3 by E16;
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 E8: 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 ; :: according to TARSKI:def 3
assume E9: c5 in [:(meet ((.: (pr1 c1,c2)) .: c4)),(union ((.: (pr2 c1,c2)) .: c4)):] ;
then E10: ( 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
E11: ( c5 `2 in c6 & c6 in (.: (pr2 c1,c2)) .: c4 ) by TARSKI:def 4;
consider c7 being set such that
E12: ( c7 in dom (.: (pr2 c1,c2)) & c7 in c4 & c6 = (.: (pr2 c1,c2)) . c7 ) by E11, FUNCT_1:def 12;
consider c8 being Subset of c1, c9 being Subset of c2 such that
E13: c7 = [:c8,c9:] by E8, E12;
E14: c7 <> {} by E11, E12, FUNCT_3:9;
c7 in bool [:c1,c2:] by E12;
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 E12, FUNCT_1:def 12;
then c8 in (.: (pr1 c1,c2)) .: c4 by E13, E14, E6;
then E15: ( c5 `1 in c8 & c5 `2 in c9 ) by E10, E11, E12, E13, E14, E6, SETFAM_1:def 1;
ex b1, b2 being set st c5 = [b1,b2] by E9, ZFMISC_1:102;
then E16: c5 in c7 by E13, E15, MCART_1:11;
c7 c= c3 by E8, E12;
hence c5 in c3 by E16;
end;

theorem E8: :: 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 E9: :: 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 } :: according to XBOOLE_0:def 10
proof
let c3 be set ; :: according to TARSKI:def 3
assume c3 in union (union c2) ;
then consider c4 being set such that
E10: ( c3 in c4 & c4 in union c2 ) by TARSKI:def 4;
consider c5 being set such that
E11: ( c4 in c5 & c5 in c2 ) by E10, TARSKI:def 4;
E12: c3 in union c5 by E10, E11, TARSKI:def 4;
union c5 in { (union b1) where B is Subset of c1 : b1 in c2 } by E11;
hence c3 in union { (union b1) where B is Subset of c1 : b1 in c2 } by E12, TARSKI:def 4;
end;
let c3 be set ; :: according to 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
E10: ( 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
E11: ( c4 = union c5 & c5 in c2 ) by E10;
consider c6 being set such that
E12: ( c3 in c6 & c6 in c5 ) by E10, E11, TARSKI:def 4;
c6 in union c2 by E11, E12, TARSKI:def 4;
hence c3 in union (union c2) by E12, TARSKI:def 4;
end;

theorem E10: :: 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 E11: union c2 = c1 ;
let c3 be Subset of c2;
let c4 be Subset of c1;
assume E12: c4 = union c3 ;
let c5 be set ; :: according to TARSKI:def 3
assume E13: c5 in c4 ` ;
then consider c6 being set such that
E14: ( c5 in c6 & c6 in c2 ) by E11, TARSKI:def 4;
not c5 in c4 by E13, XBOOLE_0:def 4;
then not c6 in c3 by E12, E14, TARSKI:def 4;
then c6 in c3 ` by E14, SUBSET_1:50;
hence c5 in union (c3 ` ) by E14, TARSKI:def 4;
end;

theorem E11: :: 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 E12: 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 ) );
E13: 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
E14: 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 E14;
end;
case E14: 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 E14;
end;
end;
end;
then consider c7 being set such that
E14: c7 in c3 and
E15: 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 E14;
thus S1[c6,c8] by E12, E15;
end;
consider c6 being Function of c2,c3 such that
E14: for b1 being set holds
( b1 in c2 implies S1[b1,c6 . b1] ) from FUNCT_2:sch 1(E13);
 take c6 ;
now
let c7 be Element of c1;
thus (c6 * c4) . c7 = c6 . (c4 . c7) by FUNCT_2:21
.= c5 . c7 by E14 ;
end;
hence c6 * c4 = c5 by FUNCT_2:113;
end;

theorem E12: :: 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 E13: :: 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 E14: :: 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 E15: :: 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 c2 --> c3 -> Function of a2,a1;
coherence
c2 --> c3 is Function of c2,c1 by FUNCOP_1:58;
end;

theorem E16: :: 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 ; :: according to TARSKI:def 3
assume c4 in union c3 ;
then consider c5 being set such that
E17: ( c4 in c5 & c5 in c3 ) by TARSKI:def 4;
c4 in union c2 by E17, TARSKI:def 4;
hence c4 in c1 ;
end;
hence union c3 is Subset of c1 ;
end;

theorem E17: :: 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; :: according to XBOOLE_0:def 10
let c5 be set ; :: according to TARSKI:def 3
assume E18: c5 in (union c3) /\ (union c4) ;
then c5 in union c3 by XBOOLE_0:def 3;
then consider c6 being set such that
E19: ( c5 in c6 & c6 in c3 ) by TARSKI:def 4;
c5 in union c4 by E18, XBOOLE_0:def 3;
then consider c7 being set such that
E20: ( c5 in c7 & c7 in c4 ) by TARSKI:def 4;
E21: ( c6 in c2 & c7 in c2 ) by E19, E20;
not c6 misses c7 by E19, E20, XBOOLE_0:3;
then c6 = c7 by E19, E21, EQREL_1:def 6;
then c6 in c3 /\ c4 by E19, E20, XBOOLE_0:def 3;
hence c5 in union (c3 /\ c4) by E19, TARSKI:def 4;
end;

theorem E18: :: 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 E19: c4 = union c3 ;
union c2 = c1 by EQREL_1:def 6;
hence c4 ` c= union (c3 ` ) by E19, E10; :: according to XBOOLE_0:def 10
let c5 be set ; :: according to TARSKI:def 3
assume c5 in union (c3 ` ) ;
then consider c6 being set such that
E20: ( c5 in c6 & c6 in c3 ` ) by TARSKI:def 4;
E21: c6 in c2 by E20;
assume not c5 in c4 ` ;
then c5 in c4 by E20, E21, SUBSET_1:50;
then consider c7 being set such that
E22: ( c5 in c7 & c7 in c3 ) by E19, TARSKI:def 4;
E23: c7 in c2 by E22;
not c6 misses c7 by E20, E22, XBOOLE_0:3;
then c6 = c7 by E21, E23, EQREL_1:def 6;
hence not verum by E20, E22, XBOOLE_0:def 4;
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 c2 -> Function of a1,a2 means :E19: :: 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;
E19: now
let c3 be set ;
assume E20: c3 in c1 ;
union c2 = c1 by EQREL_1:def 6;
then ex b1 being set st
( c3 in b1 & b1 in c2 ) by E20, 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
E20: for b1 being set holds
( b1 in c1 implies S1[b1,c3 . b1] ) from FUNCT_2:sch 1(E19);
 take c3 ;
let c4 be Element of c1;
thus c4 in c3 . c4 by E20;
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
E19: for b1 being Element of c1 holds b1 in c3 . b1 and
E20: for b1 being Element of c1 holds b1 in c4 . b1 ;
now
let c5 be Element of c1;
E21: ( 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 E19, E20;
then not c3 . c5 misses c4 . c5 by XBOOLE_0:3;
hence c3 . c5 = c4 . c5 by E21, EQREL_1:def 6;
end;
hence c3 = c4 by FUNCT_2:113;
end;
end;

:: deftheorem E19 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 E20: :: 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 E21: c3 in c4 ;
E22: (proj c2) . c3 is Subset of c1 by TARSKI:def 3;
c3 in (proj c2) . c3 by E19;
then not (proj c2) . c3 misses c4 by E21, XBOOLE_0:3;
hence c4 = (proj c2) . c3 by E22, EQREL_1:def 6;
end;

theorem E21: :: 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} :: according to XBOOLE_0:def 10
proof
let c4 be set ; :: according to TARSKI:def 3
assume E22: c4 in c3 ;
then (proj c2) . c4 = c3 by E20;
then (proj c2) . c4 in {c3} by TARSKI:def 1;
hence c4 in (proj c2) " {c3} by E22, FUNCT_2:46;
end;
let c4 be set ; :: according to TARSKI:def 3
assume E22: 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 E22, E19;
end;

theorem E22: :: 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 :: according to XBOOLE_0:def 10
proof
let c4 be set ; :: according to TARSKI:def 3
assume E23: c4 in (proj c2) " c3 ;
then E24: (proj c2) . c4 in c3 by FUNCT_2:46;
c4 in (proj c2) . c4 by E23, E19;
hence c4 in union c3 by E24, TARSKI:def 4;
end;
let c4 be set ; :: according to TARSKI:def 3
assume c4 in union c3 ;
then consider c5 being set such that
E23: ( c4 in c5 & c5 in c3 ) by TARSKI:def 4;
E24: c5 in c2 by E23;
then (proj c2) . c4 = c5 by E23, E20;
hence c4 in (proj c2) " c3 by E23, E24, FUNCT_2:46;
end;

theorem E23: :: 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
E24: c5 in c4 by SUBSET_1:10;
take c5 ;
thus (proj c2) . c5 = c3 by E24, E20;
end;

theorem E24: :: 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 E25: 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; :: according to XBOOLE_0:def 10
let c4 be set ; :: according to TARSKI:def 3
assume E26: c4 in (proj c2) " ((proj c2) .: c3) ;
then reconsider c5 = c4 as Element of c1 ;
(proj c2) . c4 in (proj c2) .: c3 by E26, FUNCT_1:def 13;
then consider c6 being Element of c1 such that
E27: ( 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 E19;
then c7 meets c3 by E27, XBOOLE_0:3;
then E28: c7 c= c3 by E25;
c5 in c7 by E27, E19;
hence c4 in c3 by E28;
end;

theorem :: BORSUK_1:34
canceled;

theorem E25: :: 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 be 1-sorted ;
let c2 be non empty 1-sorted ;
let c3 be Element of c2;
func c1 --> c3 -> Function of a1,a2 equals :: BORSUK_1:def 2
the carrier of a1 --> a3;
coherence
the carrier of c1 --> c3 is Function of c1,c2 ;
end;

:: deftheorem defines --> BORSUK_1:def 2 :
for b1 being 1-sorted
for b2 being non empty 1-sorted
for b3 being Element of b2 holds b1 --> b3 = the carrier of b1 --> b3;

theorem E26: :: BORSUK_1:36
for b1 being TopSpace
for b2 being non empty TopSpace
for b3 being Point of b2 holds b1 --> b3 is continuous
proof
let c1 be TopSpace;
let c2 be non empty TopSpace;
let c3 be Point of c2;
set c4 = c1 --> c3;
set c5 = [#] c1;
let c6 be Subset of c2; :: according to PRE_TOPC:def 12
assume c6 is closed ;
per cases not ( not c3 in c6 & c3 in c6 ) ;
suppose c3 in c6 ;
then (c1 --> c3) " c6 = the carrier of c1 by FUNCOP_1:20
.= [#] c1 ;
hence (c1 --> c3) " c6 is closed ;
end;
suppose not c3 in c6 ;
then (c1 --> c3) " c6 = {} by FUNCOP_1:22
.= {} c1 ;
hence (c1 --> c3) " c6 is closed ;
end;
end;
end;

registration
let c1 be TopSpace;
let c2 be non empty TopSpace;
let c3 be Point of c2;
cluster a1 --> a3 -> continuous ;
coherence
c1 --> c3 is continuous by E26;
end;

definition
let c1, c2 be non empty TopSpace;
let c3 be Function of c1,c2;
redefine attr a3 is continuous means :: BORSUK_1:def 3
for b1 being Point of a1
for b2 being a_neighborhood of a3