let A be finite Ordinal-Sequence; :: thesis: A . 0 c= Sum^ A
defpred S₁[ finite Sequence] means for A being finite Ordinal-Sequence st $1 = A holds
A . 0 c= Sum^ A;
A1: S₁[ {} ] ;
A2: for f being finite Sequence
for x being object st S₁[f] holds
S₁[f ^ <%x%>]

proof

let f be finite Sequence; :: thesis: for x being object st S₁[f] holds
S₁[f ^ <%x%>]
let x be object ; :: thesis: ( S₁[f] implies S₁[f ^ <%x%>] )
assume A3: S₁[f] ; :: thesis: S₁[f ^ <%x%>]
let g be finite Ordinal-Sequence; :: thesis: ( f ^ <%x%> = g implies g . 0 c= Sum^ g )
consider b being Ordinal such that
A4: rng g c= b by ORDINAL2:def 4;
assume A5: g = f ^ <%x%> ; :: thesis: g . 0 c= Sum^ g
then rng g = (rng f) \/ (rng <%x%>) by AFINSQ_1:26;
then A6: ( rng f c= b & rng <%x%> c= b ) by A4, XBOOLE_1:11;
then reconsider f9 = f as finite Ordinal-Sequence by ORDINAL2:def 4;
rng <%x%> = {x} by AFINSQ_1:33;
then x in b by A6, ZFMISC_1:31;
then reconsider x = x as Ordinal ;

per cases ( f = {} or f <> {} ) ;

suppose f = {} ; :: thesis: g . 0 c= Sum^ g

then g = {} ^ <%x%> by A5;
then g = <%x%> ;
then ( g . 0 = x & Sum^ g = x ) by Th53;
hence g . 0 c= Sum^ g ; :: thesis: verum

end;

suppose f <> {} ; :: thesis: g . 0 c= Sum^ g

then ( 0 in dom f9 & Sum^ g = (Sum^ f9) +^ x ) by A5, Th54, ORDINAL3:8;
then ( g . 0 = f9 . 0 & f9 . 0 c= Sum^ f9 & Sum^ f9 c= Sum^ g ) by A3, A5, ORDINAL3:24, ORDINAL4:def 1;
hence g . 0 c= Sum^ g ; :: thesis: verum

end;

end;

end;

for f being finite Sequence holds S₁[f] from AFINSQ_1:sch 3(A1, A2);
hence A . 0 c= Sum^ A ; :: thesis: verum