begin
definition
let v1,
v2 be
FinSequence of
REAL ;
assume A1:
v1 <> {}
;
existence
ex b1 being Matrix of (TOP-REAL 2) st
( len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds
b1 * (n,m) = |[(v1 . n),(v2 . m)]| ) )
uniqueness
for b1, b2 being Matrix of (TOP-REAL 2) st len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds
b1 * (n,m) = |[(v1 . n),(v2 . m)]| ) & len b2 = len v1 & width b2 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b2 holds
b2 * (n,m) = |[(v1 . n),(v2 . m)]| ) holds
b1 = b2
end;