set F = FGPrIso (s,t);
let a, b be Element of (pi_1 ([:S,T:],[s,t])); :: according to GROUP_6:def 6 :: thesis: (FGPrIso (s,t)) . (a * b) = ((FGPrIso (s,t)) . a) * ((FGPrIso (s,t)) . b)
consider la being Loop of [s,t] such that
A1: a = Class ((EqRel ([:S,T:],[s,t])),la) and
A2: (FGPrIso (s,t)) . a = <*(Class ((EqRel (S,s)),(pr1 la))),(Class ((EqRel (T,t)),(pr2 la)))*> by Def2;
consider lb being Loop of [s,t] such that
A3: b = Class ((EqRel ([:S,T:],[s,t])),lb) and
A4: (FGPrIso (s,t)) . b = <*(Class ((EqRel (S,s)),(pr1 lb))),(Class ((EqRel (T,t)),(pr2 lb)))*> by Def2;
reconsider B1 = Class ((EqRel (T,t)),(pr2 la)), B2 = Class ((EqRel (T,t)),(pr2 lb)) as Element of (pi_1 (T,t)) by TOPALG_1:47;
reconsider A1 = Class ((EqRel (S,s)),(pr1 la)), A2 = Class ((EqRel (S,s)),(pr1 lb)) as Element of (pi_1 (S,s)) by TOPALG_1:47;
consider lab being Loop of [s,t] such that
A5: a * b = Class ((EqRel ([:S,T:],[s,t])),lab) and
A6: (FGPrIso (s,t)) . (a * b) = <*(Class ((EqRel (S,s)),(pr1 lab))),(Class ((EqRel (T,t)),(pr2 lab)))*> by Def2;
a * b = Class ((EqRel ([:S,T:],[s,t])),(la + lb)) by A1, A3, TOPALG_1:61;
then A7: lab,la + lb are_homotopic by A5, TOPALG_1:46;
then A8: pr1 lab, pr1 (la + lb) are_homotopic by Th19;
A9: pr2 lab, pr2 (la + lb) are_homotopic by A7, Th20;
A10: B1 * B2 = Class ((EqRel (T,t)),((pr2 la) + (pr2 lb))) by TOPALG_1:61
.= Class ((EqRel (T,t)),(pr2 (la + lb))) by Th25
.= Class ((EqRel (T,t)),(pr2 lab)) by A9, TOPALG_1:46 ;
A1 * A2 = Class ((EqRel (S,s)),((pr1 la) + (pr1 lb))) by TOPALG_1:61
.= Class ((EqRel (S,s)),(pr1 (la + lb))) by Th23
.= Class ((EqRel (S,s)),(pr1 lab)) by A8, TOPALG_1:46 ;
hence (FGPrIso (s,t)) . (a * b) = ((FGPrIso (s,t)) . a) * ((FGPrIso (s,t)) . b) by A2, A4, A6, A10, GROUP_7:29; :: thesis: verum