let i be Nat; for e1, e2 being Element of i -tuples_on REAL
for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
let e1, e2 be Element of i -tuples_on REAL; for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
let f1, f2 be Element of i -tuples_on the carrier of F_Real; ( e1 = f1 & e2 = f2 implies mlt (e1,e2) = mlt (f1,f2) )
assume A1:
( e1 = f1 & e2 = f2 )
; mlt (e1,e2) = mlt (f1,f2)
A2: dom (mlt (e1,e2)) =
Seg (len (mlt (e1,e2)))
by FINSEQ_1:def 3
.=
Seg i
by CARD_1:def 7
.=
Seg (len (mlt (f1,f2)))
by CARD_1:def 7
.=
dom (mlt (f1,f2))
by FINSEQ_1:def 3
;
for i being Nat st i in dom (mlt (e1,e2)) holds
(mlt (e1,e2)) . i = (mlt (f1,f2)) . i
proof
let i be
Nat;
( i in dom (mlt (e1,e2)) implies (mlt (e1,e2)) . i = (mlt (f1,f2)) . i )
assume A3:
i in dom (mlt (e1,e2))
;
(mlt (e1,e2)) . i = (mlt (f1,f2)) . i
(
e1 . i in REAL &
e2 . i in REAL )
by XREAL_0:def 1;
then reconsider a1 =
e1 . i,
a2 =
e2 . i as
Element of
F_Real by VECTSP_1:def 5;
thus (mlt (e1,e2)) . i =
a1 * a2
by RVSUM_1:59
.=
(mlt (f1,f2)) . i
by A1, A2, A3, FVSUM_1:60
;
verum
end;
hence
mlt (e1,e2) = mlt (f1,f2)
by A2, FINSEQ_1:13; verum