let H be RealUnitarySpace; :: thesis: ex F being Function of [: the carrier of H,( the carrier of H *):],( the carrier of H *) st
for x being Point of H
for e being FinSequence of H ex Fe being FinSequence of H st
( Fe = F . (x,e) & Fe = (x .|. e) (*) e )
set CH = the carrier of H;
defpred S₁[ object , object , object ] means ex x being Point of H ex e being FinSequence of the carrier of H st
( $1 = x & $2 = e & ex Fe being FinSequence of the carrier of H st
( Fe = $3 & Fe = (x .|. e) (*) e ) );
A1: for x, y being object st x in the carrier of H & y in the carrier of H * holds
ex z being object st
( z in the carrier of H * & S₁[x,y,z] )

proof

let x0, y0 be object ; :: thesis: ( x0 in the carrier of H & y0 in the carrier of H * implies ex z being object st
( z in the carrier of H * & S₁[x0,y0,z] ) )
assume A2: ( x0 in the carrier of H & y0 in the carrier of H * ) ; :: thesis: ex z being object st
( z in the carrier of H * & S₁[x0,y0,z] )
then reconsider xn = x0 as Point of H ;
reconsider e = y0 as FinSequence of the carrier of H by A2, FINSEQ_1:def 11;
defpred S₂[ object , object ] means $2 = (xn .|. (e /. $1)) * (e /. $1);
A3: for k being Nat st k in Seg (len e) holds
ex z being Element of the carrier of H st S₂[k,z] ;
consider Fe being FinSequence of the carrier of H such that
A4: ( dom Fe = Seg (len e) & ( for k being Nat st k in Seg (len e) holds
S₂[k,Fe . k] ) ) from FINSEQ_1:sch 5(A3);
A5: len Fe = len e by A4, FINSEQ_1:def 3;
A6: for i being Nat st 1 <= i & i <= len Fe holds
Fe . i = (xn .|. (e /. i)) * (e /. i)

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len Fe implies Fe . i = (xn .|. (e /. i)) * (e /. i) )
assume ( 1 <= i & i <= len Fe ) ; :: thesis: Fe . i = (xn .|. (e /. i)) * (e /. i)
then i in Seg (len Fe) ;
hence Fe . i = (xn .|. (e /. i)) * (e /. i) by A4, A5; :: thesis: verum

end;

take Fe ; :: thesis: ( Fe in the carrier of H * & S₁[x0,y0,Fe] )
thus Fe in the carrier of H * by FINSEQ_1:def 11; :: thesis: S₁[x0,y0,Fe]
Fe = (xn .|. e) (*) e

proof

thus len Fe = len ((xn .|. e) (*) e) by A5, DefR; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len Fe or Fe . b₁ = ((xn .|. e) (*) e) . b₁ )
let i be Nat; :: thesis: ( not 1 <= i or not i <= len Fe or Fe . i = ((xn .|. e) (*) e) . i )
assume E1: ( 1 <= i & i <= len Fe ) ; :: thesis: Fe . i = ((xn .|. e) (*) e) . i
len (xn .|. e) = len e by DefSK;
then i in dom (xn .|. e) by A5, E1, FINSEQ_3:25;
then E2: (xn .|. e) /. i = (xn .|. e) . i by PARTFUN1:def 6;
thus Fe . i = (xn .|. (e /. i)) * (e /. i) by A6, E1
.= ((xn .|. e) /. i) * (e /. i) by E1, E2, A5, DefSK
.= ((xn .|. e) (*) e) . i by E1, A5, DefR ; :: thesis: verum

end;

hence S₁[x0,y0,Fe] ; :: thesis: verum

end;

consider F being Function of [: the carrier of H,( the carrier of H *):],( the carrier of H *) such that
A7: for z, y being object st z in the carrier of H & y in the carrier of H * holds
S₁[z,y,F . (z,y)] from BINOP_1:sch 1(A1);
take F ; :: thesis: for x being Point of H
for e being FinSequence of H ex Fe being FinSequence of H st
( Fe = F . (x,e) & Fe = (x .|. e) (*) e )
let z be Point of H; :: thesis: for e being FinSequence of H ex Fe being FinSequence of H st
( Fe = F . (z,e) & Fe = (z .|. e) (*) e )
let e0 be FinSequence of the carrier of H; :: thesis: ex Fe being FinSequence of H st
( Fe = F . (z,e0) & Fe = (z .|. e0) (*) e0 )
e0 in the carrier of H * by FINSEQ_1:def 11;
then S₁[z,e0,F . (z,e0)] by A7;
hence ex Fe being FinSequence of H st
( Fe = F . (z,e0) & Fe = (z .|. e0) (*) e0 ) ; :: thesis: verum