let F be FinSequence of REAL ; :: thesis: for F1, F2 being real-valued FinSequence st F = multreal .: (F1,F2) holds
F = multreal .: (F2,F1)
let F1, F2 be real-valued FinSequence; :: thesis: ( F = multreal .: (F1,F2) implies F = multreal .: (F2,F1) )
reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2;
A5: dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;
then A6: [:(rng F4),(rng F3):] c= dom multreal by ZFMISC_1:96;
[:(rng F3),(rng F4):] c= dom multreal by A5, ZFMISC_1:96;
then A7: dom (multreal .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69
.= dom (multreal .: (F2,F1)) by A6, FUNCOP_1:69 ;
assume A8: F = multreal .: (F1,F2) ; :: thesis: F = multreal .: (F2,F1)
for z being set st z in dom (multreal .: (F2,F1)) holds
F . z = multreal . ((F2 . z),(F1 . z))

proof

let z be set ; :: thesis: ( z in dom (multreal .: (F2,F1)) implies F . z = multreal . ((F2 . z),(F1 . z)) )
assume A9: z in dom (multreal .: (F2,F1)) ; :: thesis: F . z = multreal . ((F2 . z),(F1 . z))
set F1z = F1 . z;
set F2z = F2 . z;
thus F . z = multreal . ((F1 . z),(F2 . z)) by A8, A7, A9, FUNCOP_1:22
.= (F1 . z) * (F2 . z) by BINOP_2:def 11
.= multreal . ((F2 . z),(F1 . z)) by BINOP_2:def 11 ; :: thesis: verum

end;

hence F = multreal .: (F2,F1) by A8, A7, FUNCOP_1:21; :: thesis: verum