let a be Real; :: thesis: for t being 1 _greater Nat ex x1, x2 being object st
( x1 in dom (F_dp1 (t,a)) & x2 in dom (F_dp1 (t,a)) & x1 <> x2 & (F_dp1 (t,a)) . x1 = (F_dp1 (t,a)) . x2 )
let t be 1 _greater Nat; :: thesis: ex x1, x2 being object st
( x1 in dom (F_dp1 (t,a)) & x2 in dom (F_dp1 (t,a)) & x1 <> x2 & (F_dp1 (t,a)) . x1 = (F_dp1 (t,a)) . x2 )
set A = dom (F_dp1 (t,a));
set B = rng (F_dp1 (t,a));
A1: ( card (rng (F_dp1 (t,a))) in card (dom (F_dp1 (t,a))) & rng (F_dp1 (t,a)) <> {} ) by Lm10;
defpred S₁[ object , object ] means ex m1 being object st
( $1 in dom (F_dp1 (t,a)) & $2 = m1 & (F_dp1 (t,a)) . $1 = m1 );
A2: for x being object st x in dom (F_dp1 (t,a)) holds
ex y being object st
( y in rng (F_dp1 (t,a)) & S₁[x,y] ) by FUNCT_1:3;
consider h being Function of (dom (F_dp1 (t,a))),(rng (F_dp1 (t,a))) such that
A3: for x being object st x in dom (F_dp1 (t,a)) holds
S₁[x,h . x] from FUNCT_2:sch 1(A2);
consider m1, m2 being object such that
A4: m1 in dom (F_dp1 (t,a)) and
A5: m2 in dom (F_dp1 (t,a)) and
A6: m1 <> m2 and
A7: h . m1 = h . m2 by A1, FINSEQ_4:65;
A9: S₁[m2,h . m2] by A3, A5;
S₁[m1,h . m1] by A3, A4;
then (F_dp1 (t,a)) . m1 = h . m2 by A7
.= (F_dp1 (t,a)) . m2 by A9 ;
hence ex x1, x2 being object st
( x1 in dom (F_dp1 (t,a)) & x2 in dom (F_dp1 (t,a)) & x1 <> x2 & (F_dp1 (t,a)) . x1 = (F_dp1 (t,a)) . x2 ) by A4, A5, A6; :: thesis: verum