let p, q be FinSequence of INT.Ring; :: thesis: for p1, q1 being FinSequence of F_Real st p = p1 & q = q1 holds
p "*" q = p1 "*" q1
let p1, q1 be FinSequence of F_Real; :: thesis: ( p = p1 & q = q1 implies p "*" q = p1 "*" q1 )
assume AS: ( p = p1 & q = q1 ) ; :: thesis: p "*" q = p1 "*" q1
A2: [:(rng p),(rng q):] c= [:INT,INT:] by ZFMISC_1:96;
A3: rng <:p,q:> c= [:(rng p),(rng q):] by FUNCT_3:51;
B1: dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;
[:INT,INT:] c= [:REAL,REAL:] by NUMBERS:15, ZFMISC_1:96;
then B2: rng <:p,q:> c= dom multreal by A2, A3, B1;
[:INT,INT:] = dom multint by FUNCT_2:def 1;
then B3: rng <:p,q:> c= dom multint by A2, A3;
multreal | (dom multint) = multint by LMLT12, FUNCT_2:def 1;
then A6: multint * <:p,q:> = multreal * <:p,q:> by LMEQ5, B3, B2;
mlt (p,q) = multint * <:p1,q1:> by AS, FUNCOP_1:def 3
.= mlt (p1,q1) by AS, A6, FUNCOP_1:def 3 ;
hence p "*" q = p1 "*" q1 by LmSign1X; :: thesis: verum