thus ( F is component-commutative implies for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi ) :: thesis: ( ( for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi ) implies F is component-commutative )

proof

assume A1: F is component-commutative ; :: thesis: for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi
let i, j be Element of I; :: thesis: for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi
let gi, gj be Element of G; :: thesis: ( i <> j & gi in F . i & gj in F . j implies gi * gj = gj * gi )
assume i <> j ; :: thesis: ( not gi in F . i or not gj in F . j or gi * gj = gj * gi )
then ex Fi, Fj being Subgroup of G st
( Fi = F . i & Fj = F . j & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) ) by A1;
hence ( not gi in F . i or not gj in F . j or gi * gj = gj * gi ) ; :: thesis: verum

end;

assume A2: for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi ; :: thesis: F is component-commutative
let i, j be object ; :: according to GROUP_20:def 2 :: thesis: for gi, gj being Element of G st i in I & j in I & i <> j holds
ex Fi, Fj being Subgroup of G st
( Fi = F . i & Fj = F . j & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) )
let gi, gj be Element of G; :: thesis: ( i in I & j in I & i <> j implies ex Fi, Fj being Subgroup of G st
( Fi = F . i & Fj = F . j & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) ) )
assume that
A3: ( i in I & j in I ) and
A4: i <> j ; :: thesis: ex Fi, Fj being Subgroup of G st
( Fi = F . i & Fj = F . j & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) )
reconsider Fi = F . i, Fj = F . j as Subgroup of G by A3, Def1;
take Fi ; :: thesis: ex Fj being Subgroup of G st
( Fi = F . i & Fj = F . j & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) )
take Fj ; :: thesis: ( Fi = F . i & Fj = F . j & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) )
thus ( Fi = F . i & Fj = F . j & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) ) by A2, A3, A4; :: thesis: verum