let I be non empty set ; :: thesis: for F being Group-Family of I
for a, b being Element of (product F) st support (a,F) misses support (b,F) holds
a * b = b * a
let F be Group-Family of I; :: thesis: for a, b being Element of (product F) st support (a,F) misses support (b,F) holds
a * b = b * a
let a, b be Element of (product F); :: thesis: ( support (a,F) misses support (b,F) implies a * b = b * a )
assume A1: support (a,F) misses support (b,F) ; :: thesis: a * b = b * a
reconsider c = a * b as Element of (product F) ;
reconsider d = b * a as Element of (product F) ;
A2: dom c = I by Th3;
A3: dom d = I by Th3;
for i being object st i in I holds
c . i = d . i

proof

let i be object ; :: thesis: ( i in I implies c . i = d . i )
assume i in I ; :: thesis: c . i = d . i
then reconsider i = i as Element of I ;
a in product F ;
then a . i in F . i by Th5;
then reconsider ai = a . i as Element of (F . i) ;
b in product F ;
then b . i in F . i by Th5;
then reconsider bi = b . i as Element of (F . i) ;

per cases ( i in support (a,F) or not i in support (a,F) ) ;

suppose i in support (a,F) ; :: thesis: c . i = d . i

then A4: not i in support (b,F) by A1, XBOOLE_0:3;
c . i = ai * bi by GROUP_7:1
.= ai * (1_ (F . i)) by A4, Def1
.= ai by GROUP_1:def 4
.= (1_ (F . i)) * ai by GROUP_1:def 4
.= bi * ai by A4, Def1
.= d . i by GROUP_7:1 ;
hence c . i = d . i ; :: thesis: verum

end;

suppose A5: not i in support (a,F) ; :: thesis: c . i = d . i

c . i = ai * bi by GROUP_7:1
.= (1_ (F . i)) * bi by A5, Def1
.= bi by GROUP_1:def 4
.= bi * (1_ (F . i)) by GROUP_1:def 4
.= bi * ai by A5, Def1
.= d . i by GROUP_7:1 ;
hence c . i = d . i ; :: thesis: verum

end;

end;

end;

hence a * b = b * a by A2, A3, FUNCT_1:2; :: thesis: verum