let f be FinSequence of REAL ; :: thesis: ( f = sqr F iff f = sqrreal * F )
sqr F = sqrreal * F
proof
dom sqrreal = REAL by FUNCT_2:def 1;
then A1: rng F c= dom sqrreal ;
A2: dom (sqr F) = dom F by VALUED_1:11
.= dom (sqrreal * F) by A1, RELAT_1:27 ;
hence len (sqr F) = len (sqrreal * F) by FINSEQ_3:29; :: according to FINSEQ_1:def 17 :: thesis: for b1 being set holds
( not 1 <= b1 or not b1 <= len (sqr F) or (sqr F) . b1 = (sqrreal * F) . b1 )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len (sqr F) or (sqr F) . k = (sqrreal * F) . k )
assume ( 1 <= k & k <= len (sqr F) ) ; :: thesis: (sqr F) . k = (sqrreal * F) . k
then A3: k in dom (sqr F) by FINSEQ_3:25;
thus (sqr F) . k = (F . k) ^2 by VALUED_1:11
.= sqrreal . (F . k) by Def2
.= (sqrreal * F) . k by A2, A3, FUNCT_1:12 ; :: thesis: verum
end;
hence ( f = sqr F iff f = sqrreal * F ) ; :: thesis: verum