A1: now :: thesis: for G being FinSequence of the carrier of L st dom G = dom p & ( for i being object st i in dom p holds
G /. i = a * (p /. i) ) holds
G = a * p

set R = (a multfield) * p;
let G be FinSequence of the carrier of L; :: thesis: ( dom G = dom p & ( for i being object st i in dom p holds
G /. i = a * (p /. i) ) implies G = a * p )
assume that
A2: dom G = dom p and
A3: for i being object st i in dom p holds
G /. i = a * (p /. i) ; :: thesis: G = a * p
A4: for k being object st k in dom G holds
G . k = ((a multfield) * p) . k

proof

let k be object ; :: thesis: ( k in dom G implies G . k = ((a multfield) * p) . k )
assume A5: k in dom G ; :: thesis: G . k = ((a multfield) * p) . k
then G . k = G /. k by PARTFUN1:def 6
.= a * (p /. k) by A2, A3, A5
.= (a multfield) . (p /. k) by FVSUM_1:49
.= (a multfield) . (p . k) by A2, A5, PARTFUN1:def 6
.= ((a multfield) * p) . k by A2, A5, FUNCT_1:13 ;
hence G . k = ((a multfield) * p) . k ; :: thesis: verum

end;

( rng p c= the carrier of L & dom (a multfield) = the carrier of L ) by FUNCT_2:def 1;
then dom G = dom ((a multfield) * p) by A2, RELAT_1:27;
then G = (a multfield) * p by A4;
hence G = a * p by FVSUM_1:def 6; :: thesis: verum

end;

set F = a * p;
A6: rng p c= dom (a multfield)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in dom (a multfield) )
dom (a multfield) = the carrier of L by FUNCT_2:def 1;
hence ( not x in rng p or x in dom (a multfield) ) ; :: thesis: verum

end;

A7: a * p = (a multfield) * p by FVSUM_1:def 6;
then A8: dom (a * p) = dom p by A6, RELAT_1:27;
for i being object st i in dom p holds
(a * p) /. i = a * (p /. i)

proof

let i be object ; :: thesis: ( i in dom p implies (a * p) /. i = a * (p /. i) )
assume A9: i in dom p ; :: thesis: (a * p) /. i = a * (p /. i)
(a * p) . i = ((a multfield) * p) . i by FVSUM_1:def 6
.= (a multfield) . (p . i) by A9, FUNCT_1:13
.= (a multfield) . (p /. i) by A9, PARTFUN1:def 6
.= a * (p /. i) by FVSUM_1:49 ;
hence (a * p) /. i = a * (p /. i) by A8, A9, PARTFUN1:def 6; :: thesis: verum

end;

hence for b₁ being FinSequence of the carrier of L holds
( b₁ = a * p iff ( dom b₁ = dom p & ( for i being object st i in dom p holds
b₁ /. i = a * (p /. i) ) ) ) by A7, A6, A1, RELAT_1:27; :: thesis: verum