let i be Nat; :: thesis: for R being Element of i -tuples_on REAL holds sqr R = mlt R,R
let R be Element of i -tuples_on REAL ; :: thesis: sqr R = mlt R,R
A1: len R = i by FINSEQ_1:def 18;
then A2: len (sqrreal * R) = i by FINSEQ_2:37;
A3: len (multreal .: R,R) = i by A1, FINSEQ_2:86;
X: dom (sqrreal * R) = Seg i by A2, FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom (sqrreal * R) implies (sqrreal * R) . j = (multreal .: R,R) . j )
assume A4: j in dom (sqrreal * R) ; :: thesis: (sqrreal * R) . j = (multreal .: R,R) . j
then A5: j in dom (sqrreal * R) ;
A6: j in dom (multreal .: R,R) by A3, A4, X, FINSEQ_1:def 3;
set r = R . j;
thus (sqrreal * R) . j = sqrreal . (R . j) by A5, FUNCT_1:22
.= (R . j) ^2 by Def2
.= multreal . (R . j),(R . j) by BINOP_2:def 11
.= (multreal .: R,R) . j by A6, FUNCOP_1:28 ; :: thesis: verum

end;

hence sqr R = mlt R,R by A2, A3, FINSEQ_2:10; :: thesis: verum