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 )

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

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 A2:
for i, j being Element of I
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;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

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