let X be Group-Sequence; :: thesis: for x, y, z being Element of (product X)
for x1, y1, z1 being FinSequence st x = x1 & y = y1 & z = z1 holds
( z = x + y iff for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j)) )
let x, y, z be Element of (product X); :: thesis: for x1, y1, z1 being FinSequence st x = x1 & y = y1 & z = z1 holds
( z = x + y iff for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j)) )
let x1, y1, z1 be FinSequence; :: thesis: ( x = x1 & y = y1 & z = z1 implies ( z = x + y iff for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j)) ) )
assume A1: ( x = x1 & y = y1 & z = z1 ) ; :: thesis: ( z = x + y iff for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j)) )
hereby :: thesis: ( ( for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j)) ) implies z = x + y )
assume A2: z = x + y ; :: thesis: for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j))
thus for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j)) :: thesis: verum
proof
let j be Element of dom (carr X); :: thesis: z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j))
thus z1 . j = ((addop X) . j) . ((x1 . j),(y1 . j)) by A1, A2, PRVECT_1:def 8
.= the addF of (X . j) . ((x1 . j),(y1 . j)) by PRVECT_1:def 12 ; :: thesis: verum
end;
end;
assume A3: for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j)) ; :: thesis: z = x + y
reconsider Ixy = x + y as FinSequence by NDIFF_5:9;
A4: dom Ixy = dom (carr X) by CARD_3:9;
for j0 being Nat st j0 in dom z1 holds
z1 . j0 = Ixy . j0
proof
let j0 be Nat; :: thesis: ( j0 in dom z1 implies z1 . j0 = Ixy . j0 )
assume j0 in dom z1 ; :: thesis: z1 . j0 = Ixy . j0
then reconsider j = j0 as Element of dom (carr X) by CARD_3:9, A1;
Ixy . j0 = ((addop X) . j) . ((x1 . j),(y1 . j)) by A1, PRVECT_1:def 8
.= the addF of (X . j) . ((x1 . j),(y1 . j)) by PRVECT_1:def 12
.= z1 . j by A3 ;
hence z1 . j0 = Ixy . j0 ; :: thesis: verum
end;
hence z = x + y by A1, CARD_3:9, A4, FINSEQ_1:13; :: thesis: verum