defpred S1[ set , set ] means ex l being Loop of [s,t] st
( $1 = Class (EqRel [:S,T:],[s,t]),l & $2 = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> );
A1:
for x being Element of (pi_1 [:S,T:],[s,t]) ex y being Element of (product <*(pi_1 S,s),(pi_1 T,t)*>) st S1[x,y]
proof
let x be
Element of
(pi_1 [:S,T:],[s,t]);
:: thesis: ex y being Element of (product <*(pi_1 S,s),(pi_1 T,t)*>) st S1[x,y]
consider l being
Loop of
[s,t] such that A2:
x = Class (EqRel [:S,T:],[s,t]),
l
by TOPALG_1:48;
set A =
Class (EqRel S,s),
(pr1 l);
set B =
Class (EqRel T,t),
(pr2 l);
A3:
the
carrier of
(product <*(pi_1 S,s),(pi_1 T,t)*>) = product (Carrier <*(pi_1 S,s),(pi_1 T,t)*>)
by GROUP_7:def 2;
A4:
dom <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> = {1,2}
by FINSEQ_1:4, FINSEQ_3:29;
A5:
dom (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) = {1,2}
by PARTFUN1:def 4;
now let x be
set ;
:: thesis: ( x in dom (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) implies <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> . x in (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) . x )assume A6:
x in dom (Carrier <*(pi_1 S,s),(pi_1 T,t)*>)
;
:: thesis: <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> . x in (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) . xA7:
ex
R being
1-sorted st
(
R = <*(pi_1 S,s),(pi_1 T,t)*> . x &
(Carrier <*(pi_1 S,s),(pi_1 T,t)*>) . x = the
carrier of
R )
by A5, A6, PRALG_1:def 13;
A8:
(
<*(pi_1 S,s),(pi_1 T,t)*> . 1
= pi_1 S,
s &
<*(pi_1 S,s),(pi_1 T,t)*> . 2
= pi_1 T,
t )
by FINSEQ_1:61;
A9:
(
<*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> . 1
= Class (EqRel S,s),
(pr1 l) &
<*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> . 2
= Class (EqRel T,t),
(pr2 l) )
by FINSEQ_1:61;
(
x = 1 or
x = 2 )
by A5, A6, TARSKI:def 2;
hence
<*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> . x in (Carrier <*(pi_1 S,s),(pi_1 T,t)*>) . x
by A7, A8, A9, TOPALG_1:48;
:: thesis: verum end;
then reconsider y =
<*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> as
Element of
(product <*(pi_1 S,s),(pi_1 T,t)*>) by A3, A4, A5, CARD_3:18;
take
y
;
:: thesis: S1[x,y]
take
l
;
:: thesis: ( x = Class (EqRel [:S,T:],[s,t]),l & y = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> )
thus
(
x = Class (EqRel [:S,T:],[s,t]),
l &
y = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> )
by A2;
:: thesis: verum
end;
ex h being Function of (pi_1 [:S,T:],[s,t]),(product <*(pi_1 S,s),(pi_1 T,t)*>) st
for x being Element of (pi_1 [:S,T:],[s,t]) holds S1[x,h . x]
from FUNCT_2:sch 3(A1);
hence
ex b1 being Function of (pi_1 [:S,T:],[s,t]),(product <*(pi_1 S,s),(pi_1 T,t)*>) st
for x being Point of (pi_1 [:S,T:],[s,t]) ex l being Loop of [s,t] st
( x = Class (EqRel [:S,T:],[s,t]),l & b1 . x = <*(Class (EqRel S,s),(pr1 l)),(Class (EqRel T,t),(pr2 l))*> )
; :: thesis: verum