let n be Nat; :: thesis: for x, y being Element of REAL n holds |.|(x,y)|.| <= |.x.| * |.y.|
let x, y be Element of REAL n; :: thesis: |.|(x,y)|.| <= |.x.| * |.y.|
( len x = n & len y = n ) by CARD_1:def 7;
hence |.|(x,y)|.| <= |.x.| * |.y.| by EUCLID_2:15; :: thesis: verum