defpred S₁[ 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 S₁[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 S₁[x,y]
consider l being Loop of [s,t] such that
A2: x = Class ((EqRel ([:S,T:],[s,t])),l) by TOPALG_1:47;
set B = Class ((EqRel (T,t)),(pr2 l));
set A = Class ((EqRel (S,s)),(pr1 l));
A3: dom (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) = {1,2} by PARTFUN1:def 2;

A4: now :: thesis: for x being object st x in dom (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) holds
<*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> . x in (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) . x

let x be object ; :: 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 A5: 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))*>) . x
A6: ( x = 1 or x = 2 ) by A5, TARSKI:def 2;
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, PRALG_1:def 15;
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 A6, TOPALG_1:47; :: thesis: verum

end;

( the carrier of (product <*(pi_1 (S,s)),(pi_1 (T,t))*>) = product (Carrier <*(pi_1 (S,s)),(pi_1 (T,t))*>) & dom <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> = {1,2} ) by FINSEQ_1:2, FINSEQ_1:89, GROUP_7:def 2;
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, CARD_3:9;
take y ; :: thesis: S₁[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 S₁[x,h . x] from FUNCT_2:sch 3(A1);
hence ex b₁ 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) & b₁ . x = <*(Class ((EqRel (S,s)),(pr1 l))),(Class ((EqRel (T,t)),(pr2 l)))*> ) ; :: thesis: verum