let X be Group-Sequence; 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); 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; ( 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 )
; ( 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 ( ( for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j)) ) implies z = x + y )
end;
assume A3:
for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j))
; 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
hence
z = x + y
by A1, CARD_3:9, A4, FINSEQ_1:13; verum