let I be non empty set ; :: thesis: for G being Group
for x being finite-support Function of I,G
for a being Element of G st I = {1,2} & x = <*a,(1_ G)*> holds
Product x = a
let G be Group; :: thesis: for x being finite-support Function of I,G
for a being Element of G st I = {1,2} & x = <*a,(1_ G)*> holds
Product x = a
let x be finite-support Function of I,G; :: thesis: for a being Element of G st I = {1,2} & x = <*a,(1_ G)*> holds
Product x = a
let a be Element of G; :: thesis: ( I = {1,2} & x = <*a,(1_ G)*> implies Product x = a )
assume A1: ( I = {1,2} & x = <*a,(1_ G)*> ) ; :: thesis: Product x = a
reconsider i1 = 1 as Element of I by A1, TARSKI:def 2;
set y = (I --> (1_ G)) +* (i1,a);
A2: dom ((I --> (1_ G)) +* (i1,a)) = dom (I --> (1_ G)) by FUNCT_7:30
.= I by FUNCOP_1:13 ;
A3: dom (I --> (1_ G)) = I by FUNCOP_1:13;
for i being object st i in dom x holds
x . i = ((I --> (1_ G)) +* (i1,a)) . i
proof
let i be object ; :: thesis: ( i in dom x implies x . i = ((I --> (1_ G)) +* (i1,a)) . i )
assume A4: i in dom x ; :: thesis: x . i = ((I --> (1_ G)) +* (i1,a)) . i
then A5: ( i = 1 or i = 2 ) by A1, TARSKI:def 2;
reconsider i0 = i as Element of I by A4;
per cases ( i = 1 or i <> 1 ) ;
suppose A6: i = 1 ; :: thesis: x . i = ((I --> (1_ G)) +* (i1,a)) . i
thus x . i = a by A1, A6, FINSEQ_1:44
.= ((I --> (1_ G)) +* (i1,a)) . i by A3, A6, FUNCT_7:31 ; :: thesis: verum
end;
suppose A7: i <> 1 ; :: thesis: x . i = ((I --> (1_ G)) +* (i1,a)) . i
hence ((I --> (1_ G)) +* (i1,a)) . i = (I --> (1_ G)) . i by FUNCT_7:32
.= 1_ G by A4, FUNCOP_1:7
.= x . i by A1, A5, A7, FINSEQ_1:44 ;
:: thesis: verum
end;
end;
end;
then x = (I --> (1_ G)) +* (i1,a) by A2, FUNCT_2:def 1;
hence Product x = a by GROUP_19:21; :: thesis: verum