let f1, f2 be Ordinal-Sequence; :: thesis: ( f1 is increasing & f2 is increasing implies ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing ) )
assume A1: ( f1 is increasing & f2 is increasing ) ; :: thesis: ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing )
then reconsider f = f1 * f2 as Ordinal-Sequence by Th12;
take f ; :: thesis: ( f = f1 * f2 & f is increasing )
thus f = f1 * f2 ; :: thesis: f is increasing
let A be Ordinal; :: according to ORDINAL2:def 16 :: thesis: for b₁ being set holds
( not A in b₁ or not b₁ in dom f or f . A in f . b₁ )
let B be Ordinal; :: thesis: ( not A in B or not B in dom f or f . A in f . B )
assume A2: ( A in B & B in dom f ) ; :: thesis: f . A in f . B
then A3: A in dom f by ORDINAL1:19;
A4: dom f c= dom f2 by RELAT_1:44;
reconsider A1 = f2 . A, B1 = f2 . B as Ordinal ;
( A1 in B1 & B1 in dom f1 ) by A1, A2, A4, FUNCT_1:21, ORDINAL2:def 16;
then ( f . A = f1 . A1 & f . B = f1 . B1 & f1 . A1 in f1 . B1 ) by A1, A2, A3, FUNCT_1:22, ORDINAL2:def 16;
hence f . A in f . B ; :: thesis: verum