defpred S_{1}[ Nat] means for X being real-valued positive-yielding XFinSequence st len X = X holds

Product X is positive ;

A1: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A1, A2);

then S_{1}[ len X]
;

hence Product X is positive ; :: thesis: verum

Product X is positive ;

A1: S

proof

A2:
for n being Nat st S
let X be real-valued positive-yielding XFinSequence; :: thesis: ( len X = 0 implies Product X is positive )

assume len X = 0 ; :: thesis: Product X is positive

then X = {} ;

hence Product X is positive by Th4; :: thesis: verum

end;assume len X = 0 ; :: thesis: Product X is positive

then X = {} ;

hence Product X is positive by Th4; :: thesis: verum

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

set n1 = n + 1;

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let X be real-valued positive-yielding XFinSequence; :: thesis: ( len X = n + 1 implies Product X is positive )

set XX = <%(X . n)%>;

assume A4: len X = n + 1 ; :: thesis: Product X is positive

then X = (X | n) ^ <%(X . n)%> by AFINSQ_1:56;

then A5: Product X = (Product (X | n)) * (Product <%(X . n)%>) by Th7

.= (Product (X | n)) * (X . n) by Th5 ;

n < n + 1 by NAT_1:13;

then ( n in dom X & len (X | n) = n ) by A4, AFINSQ_1:54, AFINSQ_1:66;

then A6: ( Product (X | n) > 0 & X . n in rng X ) by A3, FUNCT_1:def 3;

then X . n > 0 by PARTFUN3:def 1;

hence Product X is positive by A5, A6; :: thesis: verum

end;set n1 = n + 1;

assume A3: S

let X be real-valued positive-yielding XFinSequence; :: thesis: ( len X = n + 1 implies Product X is positive )

set XX = <%(X . n)%>;

assume A4: len X = n + 1 ; :: thesis: Product X is positive

then X = (X | n) ^ <%(X . n)%> by AFINSQ_1:56;

then A5: Product X = (Product (X | n)) * (Product <%(X . n)%>) by Th7

.= (Product (X | n)) * (X . n) by Th5 ;

n < n + 1 by NAT_1:13;

then ( n in dom X & len (X | n) = n ) by A4, AFINSQ_1:54, AFINSQ_1:66;

then A6: ( Product (X | n) > 0 & X . n in rng X ) by A3, FUNCT_1:def 3;

then X . n > 0 by PARTFUN3:def 1;

hence Product X is positive by A5, A6; :: thesis: verum

then S

hence Product X is positive ; :: thesis: verum