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)) )

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

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 A3:
for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j))
; :: thesis: z = x + yassume 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

end;thus for j being Element of dom (carr X) holds z1 . j = the addF of (X . j) . ((x1 . j),(y1 . j)) :: thesis: verum

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

hence
z = x + y
by A1, CARD_3:9, A4, FINSEQ_1:13; :: thesis: verum
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;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