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 | (support (b,F))) = a * b
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 | (support (b,F))) = a * b
let a, b be Element of (product F); :: thesis: ( support (a,F) misses support (b,F) implies a +* (b | (support (b,F))) = a * b )
assume A1: support (a,F) misses support (b,F) ; :: thesis: a +* (b | (support (b,F))) = a * b
reconsider c = a +* (b | (support (b,F))) as Function ;
reconsider d = a * b as Element of (product F) ;
A2: dom a = I by Th3;
A3: dom b = I by Th3;
A5: dom c = (dom a) \/ (dom (b | (support (b,F)))) by FUNCT_4:def 1
.= I by A2, A3, RELAT_1:60, XBOOLE_1:12 ;
A6: dom d = I by Th3;
A8: dom (b | (support (b,F))) = support (b,F) by A3, RELAT_1:62;
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 & b in product F ) ;
then ( a . i in F . i & b . i in F . i ) by Th5;
then reconsider ai = a . i, bi = b . i as Element of (F . i) ;
per cases ( not i in support (b,F) or i in support (b,F) ) ;
suppose A9: not i in support (b,F) ; :: thesis: c . i = d . i
c . i = a . i by A8, A9, FUNCT_4:11
.= ai * (1_ (F . i)) by GROUP_1:def 4
.= ai * bi by A9, Def1
.= d . i by GROUP_7:1 ;
hence c . i = d . i ; :: thesis: verum
end;
suppose A11: i in support (b,F) ; :: thesis: c . i = d . i
then A12: not i in support (a,F) by A1, XBOOLE_0:3;
c . i = (b | (support (b,F))) . i by A8, A11, FUNCT_4:13
.= bi by A11, FUNCT_1:49
.= (1_ (F . i)) * bi by GROUP_1:def 4
.= ai * bi by A12, Def1
.= d . i by GROUP_7:1 ;
hence c . i = d . i ; :: thesis: verum
end;
end;
end;
hence a +* (b | (support (b,F))) = a * b by A5, A6, FUNCT_1:2; :: thesis: verum