deffunc H₁( Nat) -> Element of REAL = In ((u .|. (x /. $1)),REAL);
consider z being FinSequence of REAL such that
A1: len z = len x and
A2: for j being Nat st j in dom z holds
z . j = H₁(j) from FINSEQ_2:sch 1();
take z ; :: thesis: ( len z = len x & ( for i being Nat st 1 <= i & i <= len x holds
z . i = u .|. (x /. i) ) )
thus len z = len x by A1; :: thesis: for i being Nat st 1 <= i & i <= len x holds
z . i = u .|. (x /. i)
let i be Nat; :: thesis: ( 1 <= i & i <= len x implies z . i = u .|. (x /. i) )
assume ( 1 <= i & i <= len x ) ; :: thesis: z . i = u .|. (x /. i)
then z . i = H₁(i) by A1, A2, FINSEQ_3:25;
hence z . i = u .|. (x /. i) ; :: thesis: verum