friends1.miz



    begin

    reserve x,y,z for object,

X for set,

i,k,n,m for Nat,

R for Relation,

P for finite Relation,

p,q for FinSequence;

    registration

      let P;

      let x be object;

      cluster ( Im (P,x)) -> finite;

      coherence

      proof

        ( Im (P,x)) c= ( rng P)

        proof

          let y be object;

          assume y in ( Im (P,x));

          then [x, y] in P by RELAT_1: 169;

          hence thesis by XTUPLE_0:def 13;

        end;

        hence thesis;

      end;

    end

    

     Lm1: (n * k) = (n *` k) & (n + k) = (n +` k)

    proof

      

       A1: k = ( card k);

      n = ( card n);

      then (n *` k) = ( card (n * k)) & (n +` k) = ( card (n + k)) by A1, CARD_2: 39, CARD_2: 38;

      hence thesis;

    end;

    theorem :: FRIENDS1:1

    

     Th1: ( card R) = ( card (R ~ ))

    proof

      defpred Q[ object, object] means for x, y st [x, y] = $1 holds [y, x] = $2;

      

       A1: for x be object st x in R holds ex y be object st Q[x, y]

      proof

        let x be object;

        assume x in R;

        then

        consider y,z be object such that

         A2: [y, z] = x by RELAT_1:def 1;

        take zy = [z, y];

        let w,t be object;

        assume

         A3: [w, t] = x;

        then w = y by A2, XTUPLE_0: 1;

        hence thesis by A3, A2, XTUPLE_0: 1;

      end;

      consider h be Function such that

       A4: ( dom h) = R & for x be object st x in R holds Q[x, (h . x)] from CLASSES1:sch 1( A1);

      

       A5: h is one-to-one

      proof

        let x1,x2 be object;

        assume that

         A6: x1 in ( dom h) and

         A7: x2 in ( dom h) and

         A8: (h . x1) = (h . x2);

        consider y2,z2 be object such that

         A9: x2 = [y2, z2] by A4, A7, RELAT_1:def 1;

        

         A10: (h . x2) = [z2, y2] by A7, A9, A4;

        consider y1,z1 be object such that

         A11: x1 = [y1, z1] by A6, A4, RELAT_1:def 1;

        

         A12: (h . x1) = [z1, y1] by A11, A6, A4;

        then z1 = z2 by A10, A8, XTUPLE_0: 1;

        hence thesis by A12, A10, A8, XTUPLE_0: 1, A11, A9;

      end;

      

       A13: ( rng h) c= (R ~ )

      proof

        let y be object;

        assume y in ( rng h);

        then

        consider x be object such that

         A14: x in ( dom h) and

         A15: (h . x) = y by FUNCT_1:def 3;

        consider t,r be object such that

         A16: x = [t, r] by A4, A14, RELAT_1:def 1;

        (h . x) = [r, t] by A14, A16, A4;

        hence thesis by A14, A16, A4, RELAT_1:def 7, A15;

      end;

      (R ~ ) c= ( rng h)

      proof

        let y,z be object;

        assume [y, z] in (R ~ );

        then

         A17: [z, y] in R by RELAT_1:def 7;

        then (h . [z, y]) = [y, z] by A4;

        hence thesis by A17, A4, FUNCT_1:def 3;

      end;

      then ( rng h) = (R ~ ) by A13;

      hence thesis by A5, WELLORD2:def 4, A4, CARD_1: 5;

    end;

    

     Lm2: R is irreflexive implies not [x, x] in R

    proof

      assume

       A1: R is irreflexive;

      assume

       A2: [x, x] in R;

      then x in ( field R) by RELAT_1: 15;

      hence contradiction by A1, RELAT_2:def 10, A2, RELAT_2:def 2;

    end;

    

     Lm3: R is symmetric & [x, y] in R implies [y, x] in R

    proof

      assume

       A1: R is symmetric;

      assume

       A2: [x, y] in R;

      then x in ( field R) & y in ( field R) by RELAT_1: 15;

      hence thesis by A1, RELAT_2:def 11, RELAT_2:def 3, A2;

    end;

    theorem :: FRIENDS1:2

    

     Th2: R is symmetric implies (R .: X) = (R " X)

    proof

      assume

       A1: R is symmetric;

      hereby

        let y be object;

        assume y in (R .: X);

        then

        consider z be object such that

         A2: [z, y] in R and

         A3: z in X by RELAT_1:def 13;

         [y, z] in R by A2, A1, Lm3;

        hence y in (R " X) by A3, RELAT_1:def 14;

      end;

      let y be object;

      assume y in (R " X);

      then

      consider z be object such that

       A4: [y, z] in R and

       A5: z in X by RELAT_1:def 14;

       [z, y] in R by A4, A1, Lm3;

      hence y in (R .: X) by A5, RELAT_1:def 13;

    end;

    

     Lm4: not k in ( dom p) implies ((p /^ k) ^ (p | k)) = p

    proof

      assume not k in ( dom p);

      per cases by FINSEQ_3: 25;

        suppose k < 1;

        then k = 0 by NAT_1: 14;

        then (p | k) = {} & (p /^ k) = p by FINSEQ_5: 28;

        hence thesis by FINSEQ_1: 34;

      end;

        suppose k > ( len p);

        then (p /^ k) = {} & (p | k) = p by RFINSEQ:def 1, FINSEQ_1: 58;

        hence thesis by FINSEQ_1: 34;

      end;

    end;

    theorem :: FRIENDS1:3

    

     Th3: ((p /^ k) ^ (p | k)) = ((q /^ n) ^ (q | n)) & k <= n & n <= ( len p) implies p = ((q /^ (n -' k)) ^ (q | (n -' k)))

    proof

      assume

       A1: ((p /^ k) ^ (p | k)) = ((q /^ n) ^ (q | n));

      set nk = (n -' k);

      set L = ( len p);

      set R = ((( rng p) \/ ( rng q)) \/ {1});

      R = (( rng p) \/ (( rng q) \/ {1})) & R = (( rng q) \/ (( rng p) \/ {1})) by XBOOLE_1: 4;

      then

      reconsider P = p, Q = q as FinSequence of R by XBOOLE_1: 7, FINSEQ_1:def 4;

      set p1k = (P /^ k), pk = (P | k), q1n = (Q /^ n), qn = (Q | n);

      assume

       A2: k <= n;

      then

       A3: (n - k) = (n -' k) by XREAL_1: 233;

      then

       A4: (nk + k) = n;

      

       A5: nk <= (nk + k) by NAT_1: 11;

      then

       A6: (n -' nk) = (n - nk) by XREAL_1: 233, A3;

      (qn ^ q1n) = q by RFINSEQ: 8;

      then

       A7: (( len q1n) + ( len qn)) = ( len q) by FINSEQ_1: 22;

      

       A8: qn = ((qn | nk) ^ (qn /^ nk)) by RFINSEQ: 8;

      assume

       A9: n <= L;

      then

      reconsider Lk = (L - k), Ln = (L - n) as Nat by A2, XXREAL_0: 2, NAT_1: 21;

      

       A10: ( len (p1k ^ pk)) = (( len p1k) + ( len pk)) by FINSEQ_1: 22;

      

       A11: (pk ^ p1k) = p by RFINSEQ: 8;

      then (( len p1k) + ( len pk)) = L by FINSEQ_1: 22;

      then L = ( len q) by A7, A10, FINSEQ_1: 22, A1;

      then

       A12: ( len q1n) = Ln by A9, RFINSEQ:def 1;

      

       A13: p1k = ((p1k | Ln) ^ (p1k /^ Ln)) by RFINSEQ: 8;

      then

       A14: (q1n ^ qn) = ((p1k | Ln) ^ ((p1k /^ Ln) ^ pk)) by A1, FINSEQ_1: 32;

      k <= L by A9, A2, XXREAL_0: 2;

      then

       A15: ( len p1k) = Lk by RFINSEQ:def 1;

      then ( len (p1k | Ln)) = Ln by A2, XREAL_1: 10, FINSEQ_1: 59;

      

      then

       A16: (p1k | Ln) = ((q1n ^ qn) | Ln) by A14, FINSEQ_5: 23

      .= q1n by A12, FINSEQ_5: 23;

      Lk >= Ln by A2, XREAL_1: 10;

      then

       A17: ( len (p1k /^ Ln)) = (Lk - Ln) by A15, RFINSEQ:def 1;

      

       A18: (qn | nk) = (((p1k /^ Ln) ^ pk) | nk) by A16, A14, FINSEQ_1: 33

      .= (p1k /^ Ln) by A17, FINSEQ_5: 23, A3;

      qn = ((p1k /^ Ln) ^ pk) by A16, A14, FINSEQ_1: 33;

      then (qn /^ nk) = pk by A18, A8, FINSEQ_1: 33;

      

      hence p = (((Q /^ nk) | k) ^ (q1n ^ (qn | nk))) by A6, FINSEQ_5: 80, A3, A13, A16, A18, A11

      .= (((Q /^ nk) | k) ^ (((Q /^ nk) /^ k) ^ (qn | nk))) by FINSEQ_6: 81, A4

      .= ((((Q /^ nk) | k) ^ ((Q /^ nk) /^ k)) ^ (qn | nk)) by FINSEQ_1: 32

      .= ((Q /^ nk) ^ (qn | nk)) by RFINSEQ: 8

      .= ((q /^ nk) ^ (q | nk)) by A5, FINSEQ_1: 82, A3;

    end;

    theorem :: FRIENDS1:4

    

     Th4: n in ( dom q) & p = ((q /^ n) ^ (q | n)) implies q = ((p /^ (( len p) -' n)) ^ (p | (( len p) -' n)))

    proof

      assume that

       A1: n in ( dom q) and

       A2: p = ((q /^ n) ^ (q | n));

      set L = ( len p);

      set R = ((( rng p) \/ ( rng q)) \/ {1});

      set Ln = (L -' n);

      R = (( rng p) \/ (( rng q) \/ {1})) & R = (( rng q) \/ (( rng p) \/ {1})) by XBOOLE_1: 4;

      then

      reconsider P = p, Q = q as FinSequence of R by XBOOLE_1: 7, FINSEQ_1:def 4;

      set q1n = (Q /^ n), qn = (Q | n), pL = (P | Ln), p1L = (P /^ Ln);

      

       A3: (qn ^ q1n) = q by RFINSEQ: 8;

      then (( len q1n) + ( len qn)) = ( len q) by FINSEQ_1: 22;

      then

       A4: L = ( len q) by FINSEQ_1: 22, A2;

      then

       A5: n <= L by FINSEQ_3: 25, A1;

      then (L - n) = (L -' n) by XREAL_1: 233;

      then

       A7: ( len q1n) = Ln by A4, A5, RFINSEQ:def 1;

      

       A8: p = (pL ^ p1L) by RFINSEQ: 8;

      pL = (q /^ n) by A2, A7, FINSEQ_5: 23;

      hence thesis by A2, A8, FINSEQ_1: 33, A3;

    end;

    theorem :: FRIENDS1:5

    

     Th5: ((p /^ k) ^ (p | k)) = ((q /^ n) ^ (q | n)) implies ex i st p = ((q /^ i) ^ (q | i))

    proof

      assume

       A1: ((p /^ k) ^ (p | k)) = ((q /^ n) ^ (q | n));

      set L = ( len p);

      set R = ((( rng p) \/ ( rng q)) \/ {1});

      R = (( rng p) \/ (( rng q) \/ {1})) & R = (( rng q) \/ (( rng p) \/ {1})) by XBOOLE_1: 4;

      then

      reconsider P = p, Q = q as FinSequence of R by XBOOLE_1: 7, FINSEQ_1:def 4;

      set p1k = (P /^ k), pk = (P | k), q1n = (Q /^ n), qn = (Q | n);

      (pk ^ p1k) = p by RFINSEQ: 8;

      then

       A2: (( len p1k) + ( len pk)) = L by FINSEQ_1: 22;

      (qn ^ q1n) = q by RFINSEQ: 8;

      then

       A3: (( len q1n) + ( len qn)) = ( len q) by FINSEQ_1: 22;

      ( len (p1k ^ pk)) = (( len p1k) + ( len pk)) by FINSEQ_1: 22;

      then

       A4: L = ( len q) by A2, A3, FINSEQ_1: 22, A1;

      per cases ;

        suppose not k in ( dom p);

        then p = ((q /^ n) ^ (q | n)) by A1, Lm4;

        hence thesis;

      end;

        suppose

         A5: not n in ( dom q) & k in ( dom p);

        then q = ((p /^ k) ^ (p | k)) by Lm4, A1;

        then p = ((q /^ (( len q) -' k)) ^ (q | (( len q) -' k))) by A5, Th4;

        hence thesis;

      end;

        suppose

         A6: n in ( dom q) & k in ( dom p) & k <= n;

        then n <= ( len p) by A4, FINSEQ_3: 25;

        then p = ((q /^ (n -' k)) ^ (q | (n -' k))) by A6, A1, Th3;

        hence thesis;

      end;

        suppose

         A7: n in ( dom q) & k in ( dom p) & k > n;

        then

         A8: (k -' n) = (k - n) by XREAL_1: 233;

        then (k -' n) <> 0 by A7;

        then

         A9: (k -' n) >= 1 by NAT_1: 14;

        

         A10: k <= ( len p) by A7, FINSEQ_3: 25;

        (k -' n) <= ((k -' n) + n) by NAT_1: 11;

        then (k -' n) <= ( len p) by A8, XXREAL_0: 2, A10;

        then

         A11: (k -' n) in ( dom p) by A9, FINSEQ_3: 25;

        q = ((p /^ (k -' n)) ^ (p | (k -' n))) by A10, A4, A7, A1, Th3;

        then p = ((q /^ (( len q) -' (k -' n))) ^ (q | (( len q) -' (k -' n)))) by A11, Th4;

        hence thesis;

      end;

    end;

    scheme :: FRIENDS1:sch1

    Sch { X() -> non empty set , n() -> non zero Nat , P[ set] } :

ex C be Cardinal st (n() *` C) = ( card { F where F be Element of (n() -tuples_on X()) : P[F] })

      provided

       A1: for p,q be FinSequence of X() st (p ^ q) is n() -element & P[(p ^ q)] holds P[(q ^ p)]

       and

       A2: for p be Element of (n() -tuples_on X()) st P[p] holds for i be Nat st i < n() & p = ((p /^ i) ^ (p | i)) holds i = 0 ;

      set T = (n() -tuples_on X());

      set XX = { F where F be Element of T : P[F] };

      per cases ;

        suppose

         A3: XX is empty;

         0 = (n() *` 0 ) by CARD_2: 20;

        hence thesis by A3;

      end;

        suppose XX is non empty;

        deffunc F( object) = { (p ^ q) where p,q be Element of (X() * ) : (q ^ p) = $1 };

        

         A4: for x be object st x in XX holds F(x) in ( bool XX)

        proof

          let x be object;

          assume x in XX;

          then

          consider pq be Element of T such that

           A5: x = pq and

           A6: P[pq];

           F(x) c= XX

          proof

            let y be object;

            

             A7: ( len pq) = n() by CARD_1:def 7;

            assume y in F(x);

            then

            consider p1,q1 be Element of (X() * ) such that

             A8: y = (p1 ^ q1) and

             A9: (q1 ^ p1) = pq by A5;

            ( len pq) = (( len q1) + ( len p1)) by A9, FINSEQ_1: 22;

            then ( len (p1 ^ q1)) = n() by A7, FINSEQ_1: 22;

            then

             A10: (p1 ^ q1) is Element of T by FINSEQ_2: 92;

            P[(p1 ^ q1)] by A6, A9, A1;

            hence thesis by A10, A8;

          end;

          hence thesis;

        end;

        consider F be Function of XX, ( bool XX) such that

         A11: for x be object st x in XX holds (F . x) = F(x) from FUNCT_2:sch 2( A4);

        set FF = (F ~ );

        

         A12: ( dom F) = XX by FUNCT_2:def 1;

        

         A13: n() in ( Seg n()) by FINSEQ_1: 3;

        for x be object st x in ( rng F) holds ( card ( Im (FF,x))) = n()

        proof

          let x be object;

          assume x in ( rng F);

          then

          consider y be object such that

           A14: y in ( dom F) and

           A15: (F . y) = x by FUNCT_1:def 3;

          consider p be Element of T such that

           A16: y = p and

           A17: P[p] by A14, A12;

          

           A18: x = F(p) by A14, A15, A16, A11;

          defpred Q[ object, object] means for i be Nat st i = $1 holds $2 = ((p /^ i) ^ (p | i));

          

           A19: ( len p) = n() by CARD_1:def 7;

          then (p /^ n()) = {} & (p | n()) = p by RFINSEQ: 27, FINSEQ_1: 58;

          then

           A20: p = ((p /^ n()) ^ (p | n())) by FINSEQ_1: 34;

          

           A21: for i be object st i in ( Seg n()) holds ex q be object st q in ( Im (FF,x)) & Q[i, q]

          proof

            let i be object;

            assume i in ( Seg n());

            then

            reconsider I = i as Nat;

            set q = (p /^ I);

            take qp = (q ^ (p | I));

            

             A22: p = ((p | I) ^ q) by RFINSEQ: 8;

            then ( len p) = (( len (p | I)) + ( len q)) by FINSEQ_1: 22;

            then

             A23: ( len qp) = n() by FINSEQ_1: 22, A19;

            then

             A24: qp is Element of T by FINSEQ_2: 92;

            

             A25: F(p) c= F(qp)

            proof

              let t be object;

              assume t in F(p);

              then

              consider t1,t2 be Element of (X() * ) such that

               A26: t = (t1 ^ t2) and

               A27: p = (t2 ^ t1);

              reconsider t12 = t as Element of (X() * ) by A26, FINSEQ_1:def 11;

              set LT = ( len t1);

              

               A28: t12 = ((t12 | LT) ^ (t12 /^ LT)) by RFINSEQ: 8;

              (t12 | LT) = t1 by A26, FINSEQ_5: 23;

              then ((t12 /^ LT) ^ (t12 | LT)) = ((p /^ n()) ^ (p | n())) by A27, A28, A26, FINSEQ_1: 33, A20;

              then

               A29: ex k2 be Nat st ((t12 /^ k2) ^ (t12 | k2)) = p by Th5;

              (qp /^ n()) = {} & (qp | n()) = qp by A23, RFINSEQ: 27, FINSEQ_1: 58;

              then ((p /^ I) ^ (p | I)) = ((qp /^ n()) ^ (qp | n())) by FINSEQ_1: 34;

              then ex k1 be Nat st ((qp /^ k1) ^ (qp | k1)) = p by Th5;

              then

              consider k3 be Nat such that

               A30: ((t12 /^ k3) ^ (t12 | k3)) = qp by A29, Th5;

              (t12 /^ k3) in (X() * ) & (t12 | k3) in (X() * ) by FINSEQ_1:def 11;

              then ((t12 | k3) ^ (t12 /^ k3)) in F(qp) by A30;

              hence thesis by RFINSEQ: 8;

            end;

            P[qp] by A1, A17, A22;

            then

             A31: qp in ( dom F) by A24, A12;

            then (F . qp) = F(qp) by A11;

            then [qp, F(qp)] in F by FUNCT_1:def 2, A31;

            then

             A32: [ F(qp), qp] in FF by RELAT_1:def 7;

             F(qp) c= F(p)

            proof

              let t be object;

              assume t in F(qp);

              then

              consider t1,t2 be Element of (X() * ) such that

               A33: t = (t1 ^ t2) and

               A34: (q ^ (p | I)) = (t2 ^ t1);

              reconsider t12 = t as Element of (X() * ) by A33, FINSEQ_1:def 11;

              set LT = ( len t1);

              

               A35: t12 = ((t12 | LT) ^ (t12 /^ LT)) by RFINSEQ: 8;

              (t12 | LT) = t1 by A33, FINSEQ_5: 23;

              then ((t12 /^ LT) ^ (t12 | LT)) = ((p /^ I) ^ (p | I)) by A34, A35, A33, FINSEQ_1: 33;

              then

              consider k be Nat such that

               A36: ((t12 /^ k) ^ (t12 | k)) = p by Th5;

              (t12 /^ k) in (X() * ) & (t12 | k) in (X() * ) by FINSEQ_1:def 11;

              then ((t12 | k) ^ (t12 /^ k)) in F(p) by A36;

              hence thesis by RFINSEQ: 8;

            end;

            then F(qp) = F(p) by A25;

            hence thesis by A32, RELAT_1: 169, A18;

          end;

          consider PR be Function of ( Seg n()), ( Im (FF,x)) such that

           A37: for i be object st i in ( Seg n()) holds Q[i, (PR . i)] from FUNCT_2:sch 1( A21);

           [y, x] in F by A14, A15, FUNCT_1:def 2;

          then [x, y] in FF by RELAT_1:def 7;

          then y in ( Im (FF,x)) by RELAT_1: 169;

          then

           A38: ( dom PR) = ( Seg n()) by FUNCT_2:def 1;

          ( Im (FF,x)) c= ( rng PR)

          proof

            let z be object;

            assume z in ( Im (FF,x));

            then [x, z] in FF by RELAT_1: 169;

            then

             A39: [z, x] in F by RELAT_1:def 7;

            then

             A40: z in ( dom F) by XTUPLE_0:def 12;

            then

             A41: (F . z) = F(z) by A11;

            consider Z be Element of T such that

             A42: z = Z and P[Z] by A40, A12;

            

             A43: Z in (X() * ) & ( <*> X()) in (X() * ) by FINSEQ_1:def 11;

            

             A44: Z = (Z ^ ( <*> X())) & (( <*> X()) ^ Z) = Z by FINSEQ_1: 34;

            x is set by TARSKI: 1;

            then (F . z) = x by A40, A39, FUNCT_1:def 2;

            then z in F(p) by A44, A43, A41, A42, A18;

            then

            consider z1,z2 be Element of (X() * ) such that

             A45: z = (z1 ^ z2) and

             A46: (z2 ^ z1) = p;

            set L = ( len z2);

            

             A47: (p | L) = z2 by A46, FINSEQ_5: 23;

            (L + ( len z1)) = ( len p) by A46, FINSEQ_1: 22;

            then

             A48: L <= ( len p) by NAT_1: 11;

            

             A49: p = ((p | L) ^ (p /^ L)) by RFINSEQ: 8;

            then

             A50: z1 = (p /^ L) by A47, A46, FINSEQ_1: 33;

            per cases by NAT_1: 14;

              suppose L = 0 ;

              then

               A51: (p | L) = {} ;

              then (p /^ L) = p by A49, FINSEQ_1: 34;

              then z = p by A45, A51, A47, A50, FINSEQ_1: 34;

              then z = (PR . n()) by A13, A37, A20;

              hence thesis by A13, A38, FUNCT_1:def 3;

            end;

              suppose L >= 1;

              then

               A52: L in ( Seg n()) by A19, A48;

              then (PR . L) = z by A47, A50, A45, A37;

              hence thesis by A52, A38, FUNCT_1:def 3;

            end;

          end;

          then

           A53: ( rng PR) = ( Im (FF,x));

          PR is one-to-one

          proof

            let i1,i2 be object;

            assume that

             A54: i1 in ( dom PR) and

             A55: i2 in ( dom PR) and

             A56: (PR . i1) = (PR . i2);

            reconsider i1, i2 as Nat by A54, A55, A38;

            

             A57: 1 <= i1 by A54, FINSEQ_1: 1;

            

             A58: 1 <= i2 by A55, FINSEQ_1: 1;

            

             A59: i2 <= n() by A55, FINSEQ_1: 1;

            

             A60: (PR . i2) = ((p /^ i2) ^ (p | i2)) & (PR . i1) = ((p /^ i1) ^ (p | i1)) by A55, A37, A54;

            then

            reconsider P1 = (PR . i1), P2 = (PR . i2) as Element of (X() * ) by FINSEQ_1:def 11;

            

             A61: i1 <= n() by A54, FINSEQ_1: 1;

            

             A62: (n() - 1) < (n() - 0 ) by XREAL_1: 15;

            per cases ;

              suppose i1 <= i2;

              then

               A63: p = ((p /^ (i2 -' i1)) ^ (p | (i2 -' i1))) & (i2 -' i1) = (i2 - i1) by Th3, A19, A59, A60, A56, XREAL_1: 233;

              (i2 - i1) <= (n() - 1) by A57, A59, XREAL_1: 13;

              then (i2 - i1) < n() by XXREAL_0: 2, A62;

              then (i2 - i1) = 0 by A17, A2, A63;

              hence thesis;

            end;

              suppose i2 <= i1;

              then

               A64: p = ((p /^ (i1 -' i2)) ^ (p | (i1 -' i2))) & (i1 -' i2) = (i1 - i2) by Th3, A19, A61, A60, A56, XREAL_1: 233;

              (i1 - i2) <= (n() - 1) by A61, A58, XREAL_1: 13;

              then (i1 - i2) < n() by XXREAL_0: 2, A62;

              then (i1 - i2) = 0 by A17, A2, A64;

              hence thesis;

            end;

          end;

          

          hence ( card ( Im (FF,x))) = ( card ( Seg n())) by A53, A38, WELLORD2:def 4, CARD_1: 5

          .= n() by FINSEQ_1: 57;

        end;

        then

         A65: ( card FF) = (( card (FF | (( dom FF) \ ( rng F)))) +` (n() *` ( card ( rng F)))) by SIMPLEX1: 1;

        ( dom FF) = ( rng F) by RELAT_1: 20;

        then (( dom FF) \ ( rng F)) = {} by XBOOLE_1: 37;

        then ( card (FF | (( dom FF) \ ( rng F)))) = 0 ;

        

        then (n() *` ( card ( rng F))) = ( card FF) by A65, CARD_2: 18

        .= ( card F) by Th1

        .= ( card XX) by A12, CARD_1: 62;

        hence thesis;

      end;

    end;

    theorem :: FRIENDS1:6

    

     Th6: for X be non empty set, A be non empty finite Subset of X holds for P be Function of X, ( bool X) st for x st x in X holds ( card (P . x)) = n holds ( card { F where F be Element of ((k + 1) -tuples_on X) : (F . 1) in A & for i st i in ( Seg k) holds (F . (i + 1)) in (P . (F . i)) }) = (( card A) * (n |^ k))

    proof

      let X be non empty set;

      let A be non empty finite Subset of X;

      let P be Function of X, ( bool X) such that

       A1: for x st x in X holds ( card (P . x)) = n;

      defpred D[ Function, Nat] means ($1 . 1) in A & for i st i in ( Seg $2) holds ($1 . (i + 1)) in (P . ($1 . i));

      defpred R[ Nat] means ( card { F where F be Element of (($1 + 1) -tuples_on X) : D[F, $1] }) = (( card A) * (n |^ $1));

      

       A2: ( dom P) = X by FUNCT_2:def 1;

      

       A3: for k st R[k] holds R[(k + 1)]

      proof

        let k;

        set k1 = (k + 1), k2 = (k1 + 1);

        set F2 = { F where F be Element of (k2 -tuples_on X) : D[F, k1] };

        set F1 = { F where F be Element of (k1 -tuples_on X) : D[F, k] };

        defpred P[ object, object] means for f be FinSequence st $2 = f holds (f | k1) = $1;

        assume

         A4: R[k];

        then

        reconsider F1 as finite set;

        consider PP be Relation such that

         A5: for x,y be object holds [x, y] in PP iff x in F1 & y in F2 & P[x, y] from RELAT_1:sch 1;

        for x st x in F1 holds ( card ( Im (PP,x))) = n

        proof

          defpred FF[ object, object] means for f be FinSequence st f = $1 holds (f . k2) = $2;

          let x;

          assume x in F1;

          then

          consider xx be Element of (k1 -tuples_on X) such that

           A6: x = xx and

           A7: D[xx, k];

          

           A8: for y be object st y in ( Im (PP,x)) holds ex z be object st z in (P . (xx . k1)) & FF[y, z]

          proof

            let y be object such that

             A9: y in ( Im (PP,x));

            

             A10: [x, y] in PP by RELAT_1: 169, A9;

            then y in F2 by A5;

            then

            consider yy be Element of ((k1 + 1) -tuples_on X) such that

             A11: y = yy and

             A12: D[yy, k1];

            take z = (yy . (k1 + 1));

            

             A13: (yy . (k1 + 1)) in (P . (yy . k1)) by FINSEQ_1: 3, A12;

            (yy | k1) = xx by A11, A10, A5, A6;

            hence thesis by FINSEQ_1: 3, FUNCT_1: 49, A13, A11;

          end;

          consider ff be Function of ( Im (PP,x)), (P . (xx . k1)) such that

           A14: for z be object st z in ( Im (PP,x)) holds FF[z, (ff . z)] from FUNCT_2:sch 1( A8);

          

           A15: ( len xx) = k1 by CARD_1:def 7;

          k1 in ( Seg k1) by FINSEQ_1: 3;

          then k1 in ( dom xx) by A15, FINSEQ_1:def 3;

          then

           A16: (xx . k1) in ( rng xx) by FUNCT_1:def 3;

          then

           A17: ( card (P . (xx . k1))) = n by A1;

          

           A18: (P . (xx . k1)) in ( rng P) by A16, A2, FUNCT_1:def 3;

          (P . (xx . k1)) c= ( rng ff)

          proof

            let z be object such that

             A19: z in (P . (xx . k1));

            reconsider Z = z as Element of X by A18, A19;

            set xz = (xx ^ <*Z*>);

            

             A20: ( len xz) = (( len xx) + 1) by FINSEQ_2: 16;

            

             A21: (xz | k1) = xx by FINSEQ_5: 23, A15;

            

             A22: P[xx, xz] & xx in F1 by FINSEQ_5: 23, A15, A7;

            reconsider xz as Element of ((k1 + 1) -tuples_on X) by A20, A15, FINSEQ_2: 92;

            

             A23: for i st i in ( Seg k1) holds (xz . (i + 1)) in (P . (xz . i))

            proof

              let i;

              assume

               A24: i in ( Seg k1);

              then

               A25: 1 <= i by FINSEQ_1: 1;

              

               A26: i <= k1 by A24, FINSEQ_1: 1;

              per cases by A26, NAT_1: 8;

                suppose

                 A27: i <= k;

                1 <= (1 + i) by NAT_1: 11;

                then (i + 1) in ( dom xx) by A27, XREAL_1: 6, A15, FINSEQ_3: 25;

                then

                 A28: (xz . (i + 1)) = (xx . (i + 1)) by FINSEQ_1:def 7;

                i < k1 by A27, NAT_1: 13;

                then

                 A29: i in ( dom xx) by A25, A15, FINSEQ_3: 25;

                (xx . (i + 1)) in (P . (xx . i)) by A27, A25, FINSEQ_1: 1, A7;

                hence thesis by A28, A29, FINSEQ_1:def 7;

              end;

                suppose

                 A30: i = k1;

                then (xz . i) = (xx . i) by A21, FINSEQ_1: 3, FUNCT_1: 49;

                hence thesis by A30, FINSEQ_1: 42, A15, A19;

              end;

            end;

            1 <= k1 by NAT_1: 11;

            then 1 in ( dom xx) by FINSEQ_3: 25, A15;

            then (xz . 1) = (xx . 1) by FINSEQ_1:def 7;

            then xz in F2 by A23, A7;

            then

             A31: [xx, xz] in PP by A5, A22;

            then

             A32: xz in ( Im (PP,xx)) by RELAT_1: 169;

            ex d be object st d in (P . (xx . k1)) & FF[xz, d] by A31, RELAT_1: 169, A6, A8;

            then

             A33: ( dom ff) = ( Im (PP,xx)) by FUNCT_2:def 1, A6;

            (ff . xz) = (xz . (k1 + 1)) by A31, RELAT_1: 169, A14, A6

            .= z by FINSEQ_1: 42, A15;

            hence thesis by A33, A32, FUNCT_1:def 3;

          end;

          then

           A34: (P . (xx . k1)) = ( rng ff);

          per cases ;

            suppose

             A35: (P . (xx . k1)) is empty;

            ( Im (PP,x)) is empty

            proof

              assume ( Im (PP,x)) is non empty;

              then

              consider d be object such that

               A36: d in ( Im (PP,x));

              ex z be object st z in (P . (xx . k1)) & FF[d, z] by A36, A8;

              hence contradiction by A35;

            end;

            hence thesis by A35, A16, A1;

          end;

            suppose

             A37: (P . (xx . k1)) is non empty;

            

             A38: ff is one-to-one

            proof

              let x1,x2 be object;

              assume that

               A39: x1 in ( dom ff) and

               A40: x2 in ( dom ff) and

               A41: (ff . x1) = (ff . x2);

              

               A42: [xx, x1] in PP by A39, RELAT_1: 169, A6;

              then x1 in F2 by A5;

              then

              consider f1 be Element of ((k1 + 1) -tuples_on X) such that

               A43: x1 = f1 and D[f1, k1];

              

               A44: ( len f1) = (k1 + 1) by CARD_1:def 7;

              (f1 | k1) = xx by A42, A43, A5;

              then

               A45: f1 = (xx ^ <*(f1 . k2)*>) by A44, FINSEQ_3: 55;

              

               A46: [xx, x2] in PP by A40, RELAT_1: 169, A6;

              then x2 in F2 by A5;

              then

              consider f2 be Element of ((k1 + 1) -tuples_on X) such that

               A47: x2 = f2 and D[f2, k1];

              

               A48: ( len f2) = (k1 + 1) by CARD_1:def 7;

              (f2 | k1) = xx by A46, A47, A5;

              then

               A49: f2 = (xx ^ <*(f2 . k2)*>) by A48, FINSEQ_3: 55;

              (f1 . k2) = (ff . x1) by A39, A14, A43;

              hence thesis by A45, A49, A40, A14, A47, A41, A43;

            end;

            ( dom ff) = ( Im (PP,x)) by A37, FUNCT_2:def 1;

            hence thesis by A38, A34, WELLORD2:def 4, CARD_1: 5, A17;

          end;

        end;

        then

         A50: ( card PP) = (( card (PP | (( dom PP) \ F1))) +` (n *` ( card F1))) by SIMPLEX1: 1;

        ( dom PP) c= F1

        proof

          let y be object;

          assume y in ( dom PP);

          then ex z be object st [y, z] in PP by XTUPLE_0:def 12;

          hence thesis by A5;

        end;

        then (( dom PP) \ F1) = {} by XBOOLE_1: 37;

        then ( card (PP | (( dom PP) \ F1))) = 0 ;

        then ( card PP) = (n *` ( card F1)) by A50, CARD_2: 18;

        

        then

         A51: ( card PP) = (n * ( card F1)) by Lm1

        .= (( card A) * (n * (n |^ k))) by A4

        .= (( card A) * (n |^ k1)) by NEWTON: 6;

        

         A52: for f2 be Element of (k2 -tuples_on X) st D[f2, k1] holds [(f2 | k1), f2] in PP

        proof

          let f2 be Element of (k2 -tuples_on X) such that

           A53: D[f2, k1];

          

           A54: f2 in F2 by A53;

          set f1 = (f2 | k1);

          

           A55: P[f1, f2];

          ( len f2) = k2 & k1 < k2 by CARD_1:def 7, NAT_1: 13;

          then ( len f1) = k1 by FINSEQ_1: 59;

          then

          reconsider f1 as Element of (k1 -tuples_on X) by FINSEQ_2: 92;

          

           A56: for i st i in ( Seg k) holds (f1 . (i + 1)) in (P . (f1 . i))

          proof

            let i;

            set i1 = (i + 1);

            assume

             A57: i in ( Seg k);

            then

             A58: 1 <= i by FINSEQ_1: 1;

            

             A59: i <= k by A57, FINSEQ_1: 1;

            then i < k1 by NAT_1: 13;

            then

             A60: (f2 . i1) in (P . (f2 . i)) & (f2 . i) = (f1 . i) by A58, FINSEQ_1: 1, A53, FUNCT_1: 49;

            1 <= i1 by NAT_1: 11;

            then i1 in ( Seg k1) by A59, XREAL_1: 6, FINSEQ_1: 1;

            hence thesis by A60, FUNCT_1: 49;

          end;

          1 <= k1 by NAT_1: 11;

          then 1 in ( Seg k1);

          then D[f1, k] by A56, FUNCT_1: 49, A53;

          then f1 in F1;

          hence thesis by A54, A55, A5;

        end;

        per cases ;

          suppose n = 0 ;

          then

           A61: (n |^ k1) = 0 by NAT_1: 11, NEWTON: 11;

          then

           A62: PP is empty by A51;

          F2 is empty

          proof

            assume F2 is non empty;

            then

            consider x2 be object such that

             A63: x2 in F2;

            ex f2 be Element of (k2 -tuples_on X) st x2 = f2 & D[f2, k1] by A63;

            hence contradiction by A52, A62;

          end;

          hence thesis by A61;

        end;

          suppose

           A64: n > 0 ;

          defpred PR[ object, object] means for x, y st $1 = [x, y] holds $2 = y;

          

           A65: for y be object st y in PP holds ex z be object st z in F2 & PR[y, z]

          proof

            let y be object;

            assume

             A66: y in PP;

            then

            consider y1,y2 be object such that

             A67: y = [y1, y2] by RELAT_1:def 1;

            take y2;

            thus thesis by XTUPLE_0: 1, A66, A67, A5;

          end;

          consider pr be Function of PP, F2 such that

           A68: for y be object st y in PP holds PR[y, (pr . y)] from FUNCT_2:sch 1( A65);

          

           A69: pr is one-to-one

          proof

            let x1,x2 be object;

            assume that

             A70: x1 in ( dom pr) and

             A71: x2 in ( dom pr) and

             A72: (pr . x1) = (pr . x2);

            consider y1,z1 be object such that

             A73: x1 = [y1, z1] by A70, RELAT_1:def 1;

            

             A74: (pr . x1) = z1 by A68, A70, A73;

            consider y2,z2 be object such that

             A75: x2 = [y2, z2] by A71, RELAT_1:def 1;

            

             A76: (pr . x2) = z2 by A68, A71, A75;

            z1 in F2 by A73, A70, A5;

            then

            consider f1 be Element of (k2 -tuples_on X) such that

             A77: z1 = f1 and D[f1, k1];

            (f1 | k1) = y1 by A73, A70, A5, A77;

            hence thesis by A71, A5, A75, A72, A73, A74, A76, A77;

          end;

          F2 is non empty

          proof

            (n |^ k1) > 0 by NEWTON: 83, A64;

            then PP is non empty by A51, XREAL_1: 129;

            then

            consider x be object such that

             A78: x in PP;

            ex y,z be object st x = [y, z] by RELAT_1:def 1, A78;

            hence thesis by A78, A5;

          end;

          then

           A79: ( dom pr) = PP by FUNCT_2:def 1;

          F2 c= ( rng pr)

          proof

            let x2 be object;

            assume x2 in F2;

            then

            consider f2 be Element of (k2 -tuples_on X) such that

             A80: x2 = f2 and

             A81: D[f2, k1];

             [(f2 | k1), f2] in PP & (pr . [(f2 | k1), f2]) = f2 by A81, A52, A68;

            hence thesis by A79, FUNCT_1:def 3, A80;

          end;

          then F2 = ( rng pr);

          hence thesis by A69, A79, WELLORD2:def 4, A51, CARD_1: 5;

        end;

      end;

      

       A82: R[ 0 ]

      proof

        deffunc P( object) = <*$1*>;

        set F0 = { F where F be Element of (( 0 + 1) -tuples_on X) : D[F, 0 ] };

        

         A83: for x be object st x in A holds P(x) in F0

        proof

          let x be object;

          assume

           A84: x in A;

          

           A85: ( len P(x)) = 1 by FINSEQ_1: 39;

          ( rng P(x)) = {x} by FINSEQ_1: 38;

          then P(x) is FinSequence of X by A84, ZFMISC_1: 31, FINSEQ_1:def 4;

          then

          reconsider Px = P(x) as Element of (( 0 + 1) -tuples_on X) by A85, FINSEQ_2: 133;

           D[Px, 0 ] by FINSEQ_1: 40, A84;

          hence thesis;

        end;

        consider f be Function of A, F0 such that

         A86: for x be object st x in A holds (f . x) = P(x) from FUNCT_2:sch 2( A83);

         P() in F0 by A83;

        then

         A87: ( dom f) = A by FUNCT_2:def 1;

        F0 c= ( rng f)

        proof

          let x be object;

          assume x in F0;

          then

           A88: ex F be Element of (( 0 + 1) -tuples_on X) st x = F & D[F, 0 ];

          then

          consider y be Element of X such that

           A89: x = <*y*> by FINSEQ_2: 97;

          

           A90: ( <*y*> . 1) = y by FINSEQ_1: 40;

          then (f . y) = x by A88, A89, A86;

          hence thesis by A88, A89, A90, A87, FUNCT_1:def 3;

        end;

        then

         A91: ( rng f) = F0;

        

         A92: f is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A93: x1 in ( dom f) & x2 in ( dom f) and

           A94: (f . x1) = (f . x2);

          

           A95: (f . x1) = P(x1) & (f . x2) = P(x2) by A93, A86;

          ( P(x1) . 1) = x1 by FINSEQ_1: 40;

          hence thesis by A95, FINSEQ_1: 40, A94;

        end;

        (n |^ 0 ) = 1 by NEWTON: 4;

        hence thesis by A91, WELLORD2:def 4, A87, A92, CARD_1: 5;

      end;

      for k holds R[k] from NAT_1:sch 2( A82, A3);

      hence thesis;

    end;

    theorem :: FRIENDS1:7

    

     Th7: ( len p) is prime & (ex i st 0 < i & i < ( len p) & p = ((p /^ i) ^ (p | i))) implies ( rng p) c= {(p . 1)}

    proof

      set L = ( len p);

      assume

       A1: L is prime;

      reconsider P = p as FinSequence of (( rng p) \/ {1}) by XBOOLE_1: 7, FINSEQ_1:def 4;

      given j be Nat such that

       A2: 0 < j and

       A3: j < L and

       A4: p = ((p /^ j) ^ (p | j));

      defpred P[ Nat] means (p . 1) = (p . (((j * $1) mod L) + 1));

      set p1j = (p /^ j), pj = (p | j);

      

       A5: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A6: P[k];

        set k1 = (k + 1), jk = ((j * k) mod L);

        (j * k1) = ((j * k) + j);

        then

         A7: ((j * k1) mod L) = ((jk + j) mod L) by NAT_D: 23;

        

         A8: ( len pj) = j by A3, FINSEQ_1: 59;

        

         A9: ( len p1j) = (L - j) by A3, RFINSEQ:def 1;

        (jk + 1) <= L by NAT_D: 1, A3, NAT_1: 13;

        then

         A10: (jk + 1) in ( dom p) by NAT_1: 11, FINSEQ_3: 25;

        per cases by A4, A10, FINSEQ_1: 25;

          suppose

           A11: (jk + 1) in ( dom p1j);

          then (jk + 1) <= (L - j) by A9, FINSEQ_3: 25;

          then ((jk + 1) + j) <= ((L - j) + j) by XREAL_1: 6;

          then ((jk + j) + 1) <= L;

          then (jk + j) < L by NAT_1: 13;

          then

           A12: ((jk + j) mod L) = (jk + j) by NAT_D: 24;

          (p . (jk + 1)) = (p1j . (jk + 1)) by A11, A4, FINSEQ_1:def 7

          .= (p . ((jk + 1) + j)) by A3, A11, RFINSEQ:def 1;

          hence thesis by A12, A7, A6;

        end;

          suppose ex n be Nat st n in ( dom pj) & (jk + 1) = (( len p1j) + n);

          then

          consider n be Nat such that

           A13: n in ( dom pj) and

           A14: (jk + 1) = (( len p1j) + n);

          ( len pj) >= n by A13, FINSEQ_3: 25;

          then

           A15: n < L by A8, A3, XXREAL_0: 2;

          reconsider n1 = (n - 1) as Nat by A13, FINSEQ_3: 25, NAT_1: 21;

          n1 < (n1 + 1) by NAT_1: 13;

          then

           A16: n1 < L by A15, XXREAL_0: 2;

          (jk + j) = ((1 * L) + n1) by A14, A9;

          

          then

           A17: ((jk + j) mod L) = (n1 mod L) by NAT_D: 21

          .= n1 by A16, NAT_D: 24;

          (p . (jk + 1)) = (pj . n) by A4, A13, A14, FINSEQ_1:def 7

          .= (p . n) by A13, FUNCT_1: 47;

          hence thesis by A17, A7, A6;

        end;

      end;

      ((j * 0 ) mod L) = 0 by NAT_D: 26;

      then

       A18: P[ 0 ];

      

       A19: for k be Nat holds P[k] from NAT_1:sch 2( A18, A5);

      let y be object;

      assume y in ( rng p);

      then

      consider m be object such that

       A20: m in ( dom p) and

       A21: (p . m) = y by FUNCT_1:def 3;

      reconsider m as Nat by A20;

      

       A22: m <= L by A20, FINSEQ_3: 25;

      reconsider m1 = (m - 1) as Nat by A20, FINSEQ_3: 25, NAT_1: 21;

      per cases ;

        suppose m = 1;

        hence thesis by A21, TARSKI:def 1;

      end;

        suppose m <> 1;

        (j gcd L) = 1

        proof

          (j gcd L) divides L by INT_2:def 2;

          then

           A23: (j gcd L) = 1 or (j gcd L) = L by A1, INT_2:def 4;

          assume (j gcd L) <> 1;

          then L divides j by A23, INT_2:def 2;

          hence contradiction by A2, NAT_D: 7, A3;

        end;

        then

        consider n be Nat such that

         A24: (((j * n) - m1) mod L) = 0 by INT_2:def 3, A3, INT_4: 16;

        

         A25: (m1 + 1) = m;

        then m1 < L by A22, NAT_1: 13;

        then (m1 mod L) = m1 by NAT_D: 24;

        then ((j * n) mod L) = m1 by A3, INT_4: 22, A24;

        then (p . 1) = (p . m) by A25, A19;

        hence thesis by TARSKI:def 1, A21;

      end;

    end;

    begin

    definition

      let R;

      let x be Element of ( field R);

      :: FRIENDS1:def1

      attr x is universal_friend means

      : Def1: for y st y in (( field R) \ {x}) holds [x, y] in R;

    end

    definition

      let R be Relation;

      :: FRIENDS1:def2

      attr R is with_universal_friend means ex x be Element of ( field R) st x is universal_friend;

    end

    notation

      let R be Relation;

      antonym R is without_universal_friend for R is with_universal_friend;

    end

    definition

      let R be Relation;

      :: FRIENDS1:def3

      attr R is friendship_graph_like means

      : Def3: for x,y be object st x in ( field R) & y in ( field R) & x <> y holds ex z be object st (( Im (R,x)) /\ ( Coim (R,y))) = {z};

    end

    registration

      cluster finite symmetric irreflexive friendship_graph_like for Relation;

      existence

      proof

        set R = the empty Relation, F = ( field R);

        for x,y be object holds x in F & y in F & [x, y] in R implies [y, x] in R;

        then

         A1: R is symmetric by RELAT_2:def 3, RELAT_2:def 11;

        for x be object holds x in F implies not [x, x] in R;

        then

         A2: R is irreflexive by RELAT_2:def 2, RELAT_2:def 10;

        for x,y be object st x in F & y in F & x <> y holds ex z be object st (( Im (R,x)) /\ ( Coim (R,y))) = {z};

        hence thesis by A1, A2, Def3;

      end;

    end

    ::$Notion-Name

    definition

      mode Friendship_Graph is finite symmetric irreflexive friendship_graph_like Relation;

    end

    reserve FSG for Friendship_Graph;

    

     Lm5: for t be object holds P is friendship_graph_like & x <> y & [x, z] in P & [z, y] in P & [x, t] in P & [t, y] in P implies z = t

    proof

      let t be object;

      assume that

       A1: (P is friendship_graph_like) & x <> y and

       A2: [x, z] in P and

       A3: [z, y] in P and

       A4: [x, t] in P and

       A5: [t, y] in P;

      x in ( field P) & y in ( field P) by A2, RELAT_1: 15, A3;

      then

      consider d be object such that

       A6: (( Im (P,x)) /\ ( Coim (P,y))) = {d} by A1;

      

       A7: y in {y} by TARSKI:def 1;

      then

       A8: t in ( Coim (P,y)) by RELAT_1:def 14, A5;

      

       A9: z in ( Coim (P,y)) by A7, RELAT_1:def 14, A3;

      z in ( Im (P,x)) by A2, RELAT_1: 169;

      then z in {d} by A9, A6, XBOOLE_0:def 4;

      then

       A10: z = d by TARSKI:def 1;

      t in ( Im (P,x)) by A4, RELAT_1: 169;

      then t in {d} by A8, A6, XBOOLE_0:def 4;

      hence thesis by A10, TARSKI:def 1;

    end;

    theorem :: FRIENDS1:8

    

     Th8: 2 divides ( card ( Im (FSG,x)))

    proof

      set I = ( Im (FSG,x));

      defpred Q[ object, object] means ex y st [$1, y] in FSG & y in I & $2 = {$1, y};

      

       A1: for x be object st x in I holds ex y be object st Q[x, y]

      proof

        let y be object;

        assume y in I;

        then

         A2: [x, y] in FSG by RELAT_1: 169;

        then

         A3: x <> y & x in ( field FSG) by Lm2, RELAT_1: 15;

        y in ( field FSG) by A2, RELAT_1: 15;

        then

        consider z be object such that

         A4: (I /\ ( Coim (FSG,y))) = {z} by A3, Def3;

        take {y, z};

        

         A5: z in {z} by TARSKI:def 1;

        ( Coim (FSG,y)) = ( Im (FSG,y)) by Th2;

        then z in ( Im (FSG,y)) by A5, A4, XBOOLE_0:def 4;

        then

         A6: [y, z] in FSG by RELAT_1: 169;

        z in I by A5, A4, XBOOLE_0:def 4;

        hence thesis by A6;

      end;

      consider h be Function such that

       A7: ( dom h) = I & for x be object st x in I holds Q[x, (h . x)] from CLASSES1:sch 1( A1);

      reconsider R = ( rng h) as finite set by A7, FINSET_1: 8;

      set H = (h ~ );

      for x st x in R holds ( card ( Im (H,x))) = 2

      proof

        let y;

        assume y in R;

        then

        consider z be object such that

         A8: z in ( dom h) and

         A9: (h . z) = y by FUNCT_1:def 3;

        consider w be object such that

         A10: [z, w] in FSG and

         A11: w in I and

         A12: y = {z, w} by A7, A8, A9;

        consider t be object such that

         A13: [w, t] in FSG and

         A14: t in I and

         A15: (h . w) = {w, t} by A11, A7;

        t = z

        proof

          

           A16: [x, w] in FSG by A11, RELAT_1: 169;

          then

           A17: x <> w & x in ( field FSG) by Lm2, RELAT_1: 15;

          w in ( field FSG) by A16, RELAT_1: 15;

          then

          consider r be object such that

           A18: (( Im (FSG,x)) /\ ( Coim (FSG,w))) = {r} by A17, Def3;

          

           A19: ( Coim (FSG,w)) = ( Im (FSG,w)) by Th2;

          then t in ( Coim (FSG,w)) by RELAT_1: 169, A13;

          then t in {r} by A14, A18, XBOOLE_0:def 4;

          then

           A20: t = r by TARSKI:def 1;

           [w, z] in FSG by A10, Lm3;

          then z in ( Coim (FSG,w)) by A19, RELAT_1: 169;

          then z in {r} by A7, A8, A18, XBOOLE_0:def 4;

          hence thesis by A20, TARSKI:def 1;

        end;

        then [w, y] in h by A12, A15, A11, A7, FUNCT_1:def 2;

        then [y, w] in H by RELAT_1:def 7;

        then

         A21: w in ( Im (H,y)) by RELAT_1: 169;

        reconsider y as set by TARSKI: 1;

        

         A22: ( Im (H,y)) c= y

        proof

          let u be object;

          assume u in ( Im (H,y));

          then [y, u] in H by RELAT_1: 169;

          then

           A23: [u, y] in h by RELAT_1:def 7;

          then

           A24: u in ( dom h) by XTUPLE_0:def 12;

          then (h . u) = y by FUNCT_1:def 2, A23;

          then ex r be object st [u, r] in FSG & r in I & y = {u, r} by A24, A7;

          hence thesis by TARSKI:def 2;

        end;

         [z, y] in h by A8, A9, FUNCT_1:def 2;

        then [y, z] in H by RELAT_1:def 7;

        then z in ( Im (H,y)) by RELAT_1: 169;

        then y c= ( Im (H,y)) by A12, A21, ZFMISC_1: 32;

        then

         A25: y = ( Im (H,y)) by A22;

        z <> w by A10, Lm2;

        hence thesis by A25, A12, CARD_2: 57;

      end;

      then

       A26: ( card H) = (( card (H | (( dom H) \ R))) +` (2 *` ( card R))) by SIMPLEX1: 1;

      ( dom H) = R by RELAT_1: 20;

      then (( dom H) \ R) = {} by XBOOLE_1: 37;

      then ( card (H | (( dom H) \ R))) = 0 ;

      then ( card H) = (2 *` ( card R)) by A26, CARD_2: 18;

      

      then (2 * ( card R)) = ( card H) by Lm1

      .= ( card h) by Th1

      .= ( card I) by A7, CARD_1: 62;

      hence thesis by INT_1:def 3;

    end;

    theorem :: FRIENDS1:9

    

     Th9: x in ( field FSG) & y in ( field FSG) & not [x, y] in FSG implies ( card ( Im (FSG,x))) = ( card ( Im (FSG,y)))

    proof

      set cx = ( card ( Im (FSG,x))), cy = ( card ( Im (FSG,y)));

      

       A1: for x, y st x in ( field FSG) & y in ( field FSG) & x <> y & not [x, y] in FSG holds (( card ( Im (FSG,x))) - 1) <= ( card ( Im (FSG,y)))

      proof

        let x, y;

        assume that

         A2: x in ( field FSG) and

         A3: y in ( field FSG) and

         A4: x <> y and

         A5: not [x, y] in FSG;

        consider z be object such that

         A6: (( Im (FSG,x)) /\ ( Coim (FSG,y))) = {z} by A2, A3, A4, Def3;

        defpred Q[ object, object] means [$1, $2] in FSG & [$2, y] in FSG;

        set Ix = ( Im (FSG,x)), Iy = ( Im (FSG,y));

        

         A7: for r be object st r in (Ix \ {z}) holds ex t be object st Q[r, t]

        proof

          let r be object;

          assume r in (Ix \ {z});

          then

           A8: [x, r] in FSG by RELAT_1: 169;

          then r in ( field FSG) by RELAT_1: 15;

          then

          consider t be object such that

           A9: (( Im (FSG,r)) /\ ( Coim (FSG,y))) = {t} by A8, A5, A3, Def3;

          take t;

          

           A10: t in {t} by TARSKI:def 1;

          ( Coim (FSG,y)) = Iy by Th2;

          then t in Iy by A10, A9, XBOOLE_0:def 4;

          then

           A11: [y, t] in FSG by RELAT_1: 169;

          t in ( Im (FSG,r)) by A10, A9, XBOOLE_0:def 4;

          hence thesis by RELAT_1: 169, A11, Lm3;

        end;

        consider h be Function such that

         A12: ( dom h) = (Ix \ {z}) & for w be object st w in (Ix \ {z}) holds Q[w, (h . w)] from CLASSES1:sch 1( A7);

        

         A13: ( rng h) c= Iy

        proof

          let t be object;

          assume t in ( rng h);

          then ex r be object st r in ( dom h) & (h . r) = t by FUNCT_1:def 3;

          then [t, y] in FSG by A12;

          then [y, t] in FSG by Lm3;

          hence thesis by RELAT_1: 169;

        end;

        z in {z} by TARSKI:def 1;

        then

         A14: z in Ix by A6, XBOOLE_0:def 4;

         not z in (Ix \ {z}) by ZFMISC_1: 56;

        

        then

         A15: (1 + ( card (Ix \ {z}))) = ( card ((Ix \ {z}) \/ {z})) by CARD_2: 41

        .= ( card Ix) by ZFMISC_1: 116, A14;

        for x1,x2 be object st x1 in ( dom h) & x2 in ( dom h) & (h . x1) = (h . x2) holds x1 = x2

        proof

          let x1,x2 be object such that

           A16: x1 in ( dom h) and

           A17: x2 in ( dom h) and

           A18: (h . x1) = (h . x2);

          

           A19: [x1, (h . x1)] in FSG & [x2, (h . x1)] in FSG by A12, A16, A17, A18;

          

           A20: (h . x1) <> x & [x, x1] in FSG by A12, A16, A5, RELAT_1: 169;

           [x, x2] in FSG by A12, A17, RELAT_1: 169;

          hence thesis by A20, Lm5, A19;

        end;

        then ( Segm ( card (Ix \ {z}))) c= ( Segm ( card Iy)) by A13, FUNCT_1:def 4, A12, CARD_1: 10;

        hence thesis by A15, NAT_1: 39;

      end;

      assume that

       A21: x in ( field FSG) & y in ( field FSG) and

       A22: not [x, y] in FSG;

      

       A23: not [y, x] in FSG by A22, Lm3;

      per cases ;

        suppose x = y or cx = cy;

        hence thesis;

      end;

        suppose

         A24: x <> y & cx <> cy;

        

         A25: ((cx + 1) - 1) = cx;

        (cy - 1) <= cx by A24, A1, A21, A23;

        then

         A26: cy <= (cx + 1) by A25, XREAL_1: 9;

        

         A27: not 2 divides 1 by INT_2: 13;

        

         A28: ((cy + 1) - 1) = cy;

        (cx - 1) <= cy by A24, A1, A21, A22;

        then

         A29: cx <= (cy + 1) by A28, XREAL_1: 9;

        

         A30: 2 divides cx & 2 divides cy by Th8;

        per cases by XXREAL_0: 1, A26;

          suppose cy < (cx + 1);

          then cy <= cx by NAT_1: 13;

          then cy < cx by A24, XXREAL_0: 1;

          then (cy + 1) <= cx by NAT_1: 13;

          then (cy + 1) = cx by A29, XXREAL_0: 1;

          hence thesis by A27, A30, INT_2: 1;

        end;

          suppose cy = (cx + 1);

          hence thesis by A30, A27, INT_2: 1;

        end;

      end;

    end;

    theorem :: FRIENDS1:10

    

     Th10: FSG is without_universal_friend & x in ( field FSG) implies ( card ( Im (FSG,x))) > 2

    proof

      assume

       A1: FSG is without_universal_friend;

      set I = ( Im (FSG,x));

      assume

       A2: x in ( field FSG);

      assume

       A3: ( card I) <= 2;

      reconsider xx = x as Element of ( field FSG) by A2;

      ( card I) = 0 or ... or ( card I) = 2 by A3;

      per cases ;

        suppose

         A4: ( card I) = 0 ;

        xx is universal_friend

        proof

          let y;

          assume

           A5: y in (( field FSG) \ {xx});

          then xx <> y by ZFMISC_1: 56;

          then

          consider z be object such that

           A6: (I /\ ( Coim (FSG,y))) = {z} by A5, Def3;

          z in {z} by TARSKI:def 1;

          then z in I by A6, XBOOLE_0:def 4;

          hence thesis by A4;

        end;

        hence thesis by A1;

      end;

        suppose ( card I) = 1;

        hence thesis by Th8, INT_2: 13;

      end;

        suppose

         A7: ( card I) = 2;

        then

        consider y1,y2 be object such that

         A8: y1 <> y2 and

         A9: I = {y1, y2} by CARD_2: 60;

        consider z1 be object such that

         A10: z1 in (( field FSG) \ {x}) and

         A11: not [xx, z1] in FSG by A1, Def1;

        

         A12: z1 <> x by A10, ZFMISC_1: 56;

        then

        consider p be object such that

         A13: (I /\ ( Coim (FSG,z1))) = {p} by A10, A2, Def3;

        

         A14: for y1,y2 be object st y1 <> y2 & I = {y1, y2} holds (I /\ ( Im (FSG,z1))) <> {y1}

        proof

          let y1,y2 be object such that

           A15: y1 <> y2 and

           A16: I = {y1, y2};

          

           A17: y1 in {y1} by TARSKI:def 1;

          assume

           A18: (I /\ ( Im (FSG,z1))) = {y1};

          then y1 in ( Im (FSG,z1)) by A17, XBOOLE_0:def 4;

          then

           A19: [z1, y1] in FSG by RELAT_1: 169;

          then y1 in ( field FSG) & z1 <> y1 by RELAT_1: 15, Lm2;

          then

          consider t be object such that

           A20: (( Im (FSG,y1)) /\ ( Coim (FSG,z1))) = {t} by Def3, A10;

          

           A21: t in {t} by TARSKI:def 1;

          then t in ( Im (FSG,y1)) by A20, XBOOLE_0:def 4;

          then

           A22: [y1, t] in FSG by RELAT_1: 169;

          then

           A23: y1 <> t by Lm2;

          

           A24: y1 in I by A16, TARSKI:def 2;

          then

           A25: [x, y1] in FSG by RELAT_1: 169;

          then

           A26: x <> y1 & y1 in ( field FSG) by Lm2, RELAT_1: 15;

          then

          consider x1x be object such that

           A27: (I /\ ( Coim (FSG,y1))) = {x1x} by A2, Def3;

          

           A28: x1x in {x1x} by TARSKI:def 1;

          then

           A29: x1x in I by A27, XBOOLE_0:def 4;

          ( Coim (FSG,y1)) = ( Im (FSG,y1)) by Th2;

          then x1x in ( Im (FSG,y1)) by A28, A27, XBOOLE_0:def 4;

          then

           A30: [y1, x1x] in FSG by RELAT_1: 169;

          then y1 <> x1x by Lm2;

          then

           A31: [y1, y2] in FSG by A29, A16, TARSKI:def 2, A30;

          y2 in I by A16, TARSKI:def 2;

          then

           A32: [xx, y2] in FSG by RELAT_1: 169;

          consider z2 be object such that

           A33: z2 in (( field FSG) \ {y1}) and

           A34: not [y1, z2] in FSG by A26, A1, Def1;

          

           A35: ( Coim (FSG,z2)) = ( Im (FSG,z2)) by Th2;

          z1 <> z2 by A19, Lm3, A34;

          then

          consider w be object such that

           A36: (( Im (FSG,z2)) /\ ( Coim (FSG,z1))) = {w} by A10, A33, Def3;

          

           A37: ( Coim (FSG,z1)) = ( Im (FSG,z1)) by Th2;

          then

           A38: t in ( Im (FSG,z1)) by A21, A20, XBOOLE_0:def 4;

          

           A39: w in {w} by TARSKI:def 1;

          then

           A40: w in ( Im (FSG,z1)) by A36, A37, XBOOLE_0:def 4;

          w in ( Im (FSG,z2)) by A39, A36, XBOOLE_0:def 4;

          then

           A41: [z2, w] in FSG by RELAT_1: 169;

          

           A42: [z1, w] in FSG by A40, RELAT_1: 169;

          

           A43: t <> w

          proof

            x <> z2 by A34, A25, Lm3;

            then

            consider s be object such that

             A44: (I /\ ( Coim (FSG,z2))) = {s} by A2, A33, Def3;

            

             A45: s in {s} by TARSKI:def 1;

            then s in ( Im (FSG,z2)) by A35, A44, XBOOLE_0:def 4;

            then [z2, s] in FSG by RELAT_1: 169;

            then

             A46: [s, z2] in FSG by Lm3;

            assume

             A47: t = w;

            

             A48: [x, y1] in FSG & [y1, z1] in FSG by A24, RELAT_1: 169, A19, Lm3;

            

             A49: y1 <> z2 & [w, z2] in FSG by A33, ZFMISC_1: 56, A41, Lm3;

            s in I by A45, A44, XBOOLE_0:def 4;

            then [y2, z2] in FSG by A46, A34, A16, TARSKI:def 2;

            then y2 = t by A49, A47, A31, A22, Lm5;

            then [y2, z1] in FSG by A42, Lm3, A47;

            hence contradiction by A48, A32, Lm5, A12, A15;

          end;

          y1 <> w by A41, Lm3, A34;

          then

           A50: ( card {y1, t, w}) = 3 by A43, CARD_2: 58, A23;

          

           A51: y1 in ( Im (FSG,z1)) by A17, A18, XBOOLE_0:def 4;

          ( card ( Im (FSG,z1))) = 2 by A11, A10, Th9, A7;

          hence thesis by ZFMISC_1: 133, A38, A40, A51, NAT_1: 43, A50;

        end;

        ( Coim (FSG,z1)) = ( Im (FSG,z1)) by Th2;

        then

         A52: p <> y1 & p <> y2 by A14, A13, A8, A9;

        p in {p} by TARSKI:def 1;

        then p in I by XBOOLE_0:def 4, A13;

        hence thesis by A52, A9, TARSKI:def 2;

      end;

    end;

    theorem :: FRIENDS1:11

    

     Th11: FSG is without_universal_friend & x in ( field FSG) & y in ( field FSG) implies ( card ( Im (FSG,x))) = ( card ( Im (FSG,y)))

    proof

      assume that

       A1: FSG is without_universal_friend and

       A2: x in ( field FSG) and

       A3: y in ( field FSG);

      per cases ;

        suppose not [x, y] in FSG;

        hence thesis by A2, A3, Th9;

      end;

        suppose

         A4: [x, y] in FSG;

        then x <> y by Lm2;

        then

         A5: ( card {x, y}) = 2 by CARD_2: 57;

        x <> y by A4, Lm2;

        then

        consider z be object such that

         A6: (( Im (FSG,x)) /\ ( Coim (FSG,y))) = {z} by A2, A3, Def3;

        

         A7: z in {z} by TARSKI:def 1;

        then

         A8: z in ( Im (FSG,x)) by A6, XBOOLE_0:def 4;

        then

         A9: [x, z] in FSG by RELAT_1: 169;

        then

         A10: z in ( field FSG) by RELAT_1: 15;

        ( Coim (FSG,y)) = ( Im (FSG,y)) by Th2;

        then

         A11: z in ( Im (FSG,y)) by A7, A6, XBOOLE_0:def 4;

        then

         A12: [y, z] in FSG by RELAT_1: 169;

        then [z, y] in FSG by Lm3;

        then

         A13: y in ( Im (FSG,z)) by RELAT_1: 169;

         [z, x] in FSG by A9, Lm3;

        then x in ( Im (FSG,z)) by RELAT_1: 169;

        then ( card (( Im (FSG,z)) \ {x, y})) = (( card ( Im (FSG,z))) - ( card {x, y})) by A13, ZFMISC_1: 32, CARD_2: 44;

        then ( card (( Im (FSG,z)) \ {x, y})) > (2 - 2) by A5, A10, A1, Th10, XREAL_1: 9;

        then ( card (( Im (FSG,z)) \ {x, y})) > 0 ;

        then (( Im (FSG,z)) \ {x, y}) is non empty;

        then

        consider w be object such that

         A14: w in (( Im (FSG,z)) \ {x, y});

        

         A15: [z, w] in FSG by A14, RELAT_1: 169;

        then

         A16: w in ( field FSG) by RELAT_1: 15;

        

         A17: not w in {x, y} by A14, XBOOLE_0:def 5;

        

         A18: x <> z by A9, Lm2;

        

         A19: not [x, w] in FSG

        proof

          

           A20: [w, z] in FSG & [y, z] in FSG by A15, Lm3, A11, RELAT_1: 169;

          assume [x, w] in FSG;

          then y = w by A20, A4, Lm5, A18;

          hence thesis by A17, TARSKI:def 2;

        end;

        

         A21: y <> z by A12, Lm2;

         not [y, w] in FSG

        proof

          assume

           A22: [y, w] in FSG;

           [x, z] in FSG by A8, RELAT_1: 169;

          then x = w by A22, A15, A4, Lm5, A21;

          hence thesis by A17, TARSKI:def 2;

        end;

        

        hence ( card ( Im (FSG,y))) = ( card ( Im (FSG,w))) by A3, A16, Th9

        .= ( card ( Im (FSG,x))) by A2, Th9, A19, A16;

      end;

    end;

    theorem :: FRIENDS1:12

    

     Th12: FSG is without_universal_friend & x in ( field FSG) implies ( card ( field FSG)) = (1 + (( card ( Im (FSG,x))) * (( card ( Im (FSG,x))) - 1)))

    proof

      defpred FSGR[ object, object] means for x, y st $1 = [x, y] holds $2 = y;

      assume that

       A1: FSG is without_universal_friend and

       A2: x in ( field FSG);

      set I = ( Im (FSG,x)), F = ( field FSG), FI = (F \ ( {x} \/ I));

      defpred R[ object, object] means $1 in I & [$1, $2] in FSG & not [x, $2] in FSG;

      consider RR be Relation such that

       A3: for y,z be object holds [y, z] in RR iff y in I & z in FI & R[y, z] from RELAT_1:sch 1;

      ( card I) > 2 by Th10, A1, A2;

      then

      reconsider cI = (( card I) - 2) as Element of NAT by NAT_1: 21;

      for y st y in I holds ( card ( Im (RR,y))) = cI

      proof

        let y be object;

        x in {x} by TARSKI:def 1;

        then x in ( {x} \/ I) by XBOOLE_0:def 3;

        then not x in FI by XBOOLE_0:def 5;

        then

         A4: not [y, x] in RR by A3;

        assume

         A5: y in I;

        then

         A6: [x, y] in FSG by RELAT_1: 169;

        then

         A7: x <> y by Lm2;

        y in F by A6, RELAT_1: 15;

        then

        consider z be object such that

         A8: (I /\ ( Coim (FSG,y))) = {z} by A7, Def3, A2;

        

         A9: z in {z} by TARSKI:def 1;

        then

         A10: z in I by XBOOLE_0:def 4, A8;

        then

         A11: [x, z] in FSG by RELAT_1: 169;

        ( Coim (FSG,y)) = ( Im (FSG,y)) by Th2;

        then

         A12: z in ( Im (FSG,y)) by A9, XBOOLE_0:def 4, A8;

        then

         A13: [y, z] in FSG by RELAT_1: 169;

        

         A14: (( Im (FSG,y)) \ {z, x}) c= ( Im (RR,y))

        proof

          let d be object;

          assume

           A15: d in (( Im (FSG,y)) \ {z, x});

          then

           A16: not d in {z, x} by XBOOLE_0:def 5;

          

           A17: [y, d] in FSG by A15, RELAT_1: 169;

          then

           A18: d in F by RELAT_1: 15;

          

           A19: not d in I

          proof

            

             A20: [d, y] in FSG & [z, y] in FSG by A17, Lm3, A13;

            assume d in I;

            then [x, d] in FSG by RELAT_1: 169;

            then d = z by A20, A11, Lm5, A7;

            hence thesis by A16, TARSKI:def 2;

          end;

          

           A21: not [x, d] in FSG

          proof

            assume

             A22: [x, d] in FSG;

            

             A23: [d, y] in FSG & [x, z] in FSG by A17, Lm3, A10, RELAT_1: 169;

             [z, y] in FSG by A13, Lm3;

            then d = z by A22, A23, Lm5, A7;

            hence thesis by A16, TARSKI:def 2;

          end;

          d <> x by A16, TARSKI:def 2;

          then not d in {x} by TARSKI:def 1;

          then not d in (I \/ {x}) by A19, XBOOLE_0:def 3;

          then d in FI by A18, XBOOLE_0:def 5;

          then [y, d] in RR by A3, A21, A5, A15, RELAT_1: 169;

          hence thesis by RELAT_1: 169;

        end;

        

         A24: not [y, z] in RR by A11, A3;

        ( Im (RR,y)) c= (( Im (FSG,y)) \ {x, z})

        proof

          let d be object;

          assume

           A25: d in ( Im (RR,y));

          then [y, d] in RR by RELAT_1: 169;

          then [y, d] in FSG by A3;

          then

           A26: d in ( Im (FSG,y)) by RELAT_1: 169;

          d <> x & d <> z by A25, A4, RELAT_1: 169, A24;

          then not d in {x, z} by TARSKI:def 2;

          hence thesis by A26, XBOOLE_0:def 5;

        end;

        then

         A27: ( Im (RR,y)) = (( Im (FSG,y)) \ {x, z}) by A14;

        y in F by A6, RELAT_1: 15;

        then

         A28: ( card ( Im (FSG,x))) = ( card ( Im (FSG,y))) by A1, A2, Th11;

         [y, x] in FSG by A6, Lm3;

        then x in ( Im (FSG,y)) by RELAT_1: 169;

        then

         A29: ( card (( Im (FSG,y)) \ {x, z})) = (( card ( Im (FSG,y))) - ( card {x, z})) by ZFMISC_1: 32, A12, CARD_2: 44;

        x <> z by A11, Lm2;

        hence thesis by A28, A27, A29, CARD_2: 57;

      end;

      then

       A30: ( card RR) = (( card (RR | (( dom RR) \ I))) +` (cI *` ( card I))) by SIMPLEX1: 1;

      ( dom RR) c= I

      proof

        let y be object;

        assume y in ( dom RR);

        then ex z be object st [y, z] in RR by XTUPLE_0:def 12;

        hence thesis by A3;

      end;

      then (( dom RR) \ I) = {} by XBOOLE_1: 37;

      then ( card (RR | (( dom RR) \ I))) = 0 ;

      

      then

       A31: ( card RR) = (cI *` ( card I)) by A30, CARD_2: 18

      .= (cI * ( card I)) by Lm1;

      

       A32: for y be object st y in RR holds ex z be object st FSGR[y, z]

      proof

        let y be object such that

         A33: y in RR;

        consider z,t be object such that

         A34: [z, t] = y by A33, RELAT_1:def 1;

        take t;

        thus thesis by XTUPLE_0: 1, A34;

      end;

      consider pr be Function such that

       A35: ( dom pr) = RR & for x be object st x in RR holds FSGR[x, (pr . x)] from CLASSES1:sch 1( A32);

      

       A36: pr is one-to-one

      proof

        let x1,x2 be object;

        assume that

         A37: x1 in ( dom pr) and

         A38: x2 in ( dom pr) and

         A39: (pr . x1) = (pr . x2);

        consider y1,t1 be object such that

         A40: x1 = [y1, t1] by A37, A35, RELAT_1:def 1;

        t1 in FI by A40, A35, A37, A3;

        then not t1 in ( {x} \/ I) by XBOOLE_0:def 5;

        then not t1 in {x} by XBOOLE_0:def 3;

        then

         A41: t1 <> x by TARSKI:def 1;

        consider y2,t2 be object such that

         A42: x2 = [y2, t2] by A35, RELAT_1:def 1, A38;

        

         A43: t1 = (pr . x1) & [y1, t1] in FSG by A37, A40, A35, A3;

        

         A44: t2 = (pr . x2) & [y2, t2] in FSG by A38, A42, A35, A3;

        y2 in I by A42, A35, A38, A3;

        then

         A45: [x, y2] in FSG by RELAT_1: 169;

        y1 in I by A40, A35, A37, A3;

        then [x, y1] in FSG by RELAT_1: 169;

        hence thesis by A41, A39, A43, A44, A45, Lm5, A40, A42;

      end;

      

       A46: FI c= ( rng pr)

      proof

        let z be object;

        assume

         A47: z in FI;

        then

         A48: not z in ( {x} \/ I) by XBOOLE_0:def 5;

        then

         A49: not z in I by XBOOLE_0:def 3;

         not z in {x} by A48, XBOOLE_0:def 3;

        then z <> x by TARSKI:def 1;

        then

        consider t be object such that

         A50: (I /\ ( Coim (FSG,z))) = {t} by A2, A47, Def3;

        

         A51: t in {t} by TARSKI:def 1;

        ( Coim (FSG,z)) = ( Im (FSG,z)) by Th2;

        then t in ( Im (FSG,z)) by A51, A50, XBOOLE_0:def 4;

        then [z, t] in FSG by RELAT_1: 169;

        then R[t, z] by A49, RELAT_1: 169, Lm3, A51, A50, XBOOLE_0:def 4;

        then [t, z] in RR & (pr . [t, z]) = z by A3, A47, A35;

        hence thesis by A35, FUNCT_1:def 3;

      end;

      ( rng pr) c= FI

      proof

        let z be object;

        assume z in ( rng pr);

        then

        consider t be object such that

         A52: t in ( dom pr) and

         A53: (pr . t) = z by FUNCT_1:def 3;

        consider t1,t2 be object such that

         A54: t = [t1, t2] by A52, A35, RELAT_1:def 1;

        (pr . t) = t2 by A52, A54, A35;

        hence thesis by A52, A54, A35, A3, A53;

      end;

      then ( rng pr) = FI by A46;

      then

       A55: (cI * ( card I)) = ( card FI) by WELLORD2:def 4, A36, A35, CARD_1: 5, A31;

      

       A56: I c= F

      proof

        let z be object;

        assume z in I;

        then [x, z] in FSG by RELAT_1: 169;

        hence thesis by RELAT_1: 15;

      end;

       not [x, x] in FSG by Lm2;

      then

       A57: ( card ( {x} \/ I)) = (( card I) + 1) by RELAT_1: 169, CARD_2: 41;

       {x} c= F by A2, ZFMISC_1: 31;

      then (cI * ( card I)) = (( card F) - ( card ( {x} \/ I))) by A56, XBOOLE_1: 8, CARD_2: 44, A55;

      then ( card F) = ((cI * ( card I)) + (( card I) + 1)) by A57;

      hence thesis;

    end;

    theorem :: FRIENDS1:13

    for x,y be Element of ( field FSG) st x is universal_friend & x <> y holds ex z be object st ( Im (FSG,y)) = {x, z} & ( Im (FSG,z)) = {x, y}

    proof

      set F = ( field FSG);

      let x,y be Element of F such that

       A1: x is universal_friend and

       A2: x <> y;

      

       A3: F is non empty

      proof

        assume F is empty;

        then x = {} & y = {} by SUBSET_1:def 1;

        hence thesis by A2;

      end;

      then

       A4: y in (F \ {x}) by A2, ZFMISC_1: 56;

      consider z be object such that

       A5: {z} = (( Im (FSG,x)) /\ ( Coim (FSG,y))) by A2, A3, Def3;

      

       A6: z in {z} by TARSKI:def 1;

      then z in ( Im (FSG,x)) by A5, XBOOLE_0:def 4;

      then

       A7: [x, z] in FSG by RELAT_1: 169;

      then

       A8: [z, x] in FSG by Lm3;

      then

       A9: x in ( Im (FSG,z)) by RELAT_1: 169;

      ( Coim (FSG,y)) = ( Im (FSG,y)) by Th2;

      then

       A10: z in ( Im (FSG,y)) by A6, A5, XBOOLE_0:def 4;

      then

       A11: [y, z] in FSG by RELAT_1: 169;

      

       A12: ( Im (FSG,y)) c= {x, z}

      proof

        let d be object;

        assume d in ( Im (FSG,y));

        then

         A13: [y, d] in FSG by RELAT_1: 169;

        assume

         A14: not d in {x, z};

        then

         A15: d <> x by TARSKI:def 2;

        d in F by A13, RELAT_1: 15;

        then d in (F \ {x}) by A15, ZFMISC_1: 56;

        then [x, d] in FSG by A1;

        then

         A16: [d, x] in FSG by Lm3;

        d <> z by A14, TARSKI:def 2;

        hence thesis by A16, A2, A13, Lm5, A11, A8;

      end;

      take z;

       [x, y] in FSG by A1, A4;

      then

       A17: [y, x] in FSG by Lm3;

      then x in ( Im (FSG,y)) by RELAT_1: 169;

      then {x, z} c= ( Im (FSG,y)) by A10, ZFMISC_1: 32;

      hence ( Im (FSG,y)) = {x, z} by A12;

      

       A18: [z, y] in FSG by A11, Lm3;

      

       A19: ( Im (FSG,z)) c= {x, y}

      proof

        let d be object;

        assume d in ( Im (FSG,z));

        then

         A20: [z, d] in FSG by RELAT_1: 169;

        assume

         A21: not d in {x, y};

        then

         A22: d <> x by TARSKI:def 2;

        d in F by A20, RELAT_1: 15;

        then d in (F \ {x}) by A22, ZFMISC_1: 56;

        then [x, d] in FSG by A1;

        then

         A23: [d, x] in FSG by Lm3;

        

         A24: x <> z by A7, Lm2;

        d <> y by A21, TARSKI:def 2;

        hence thesis by A23, A24, A20, Lm5, A17, A18;

      end;

      y in ( Im (FSG,z)) by A18, RELAT_1: 169;

      then {x, y} c= ( Im (FSG,z)) by A9, ZFMISC_1: 32;

      hence thesis by A19;

    end;

    begin

    ::$Notion-Name

    theorem :: FRIENDS1:14

    FSG is non empty implies FSG is with_universal_friend

    proof

      set F = ( field FSG);

      defpred Q1[ FinSequence] means for i be Nat st 1 <= i & i < ( len $1) holds [($1 . i), ($1 . (i + 1))] in FSG;

      deffunc W( object) = ( Im (FSG,$1));

      assume

       A1: FSG is non empty without_universal_friend;

      then

      consider x be object such that

       A2: x in F by XBOOLE_0:def 1;

      reconsider F as non empty finite set by A2;

      set m = ( card ( Im (FSG,x)));

      reconsider m1 = (m - 1) as Nat by Th10, A1, A2, NAT_1: 20;

      (m1 + 1) > 2 by Th10, A1, A2;

      then

      consider p be Element of NAT such that

       A3: p is prime and

       A4: p divides m1 by NAT_1: 13, INT_2: 31;

      

       A5: p > 1 by A3, INT_2:def 4;

      reconsider p as non zero Element of NAT by A3, INT_2:def 4;

      

       A6: 2 divides m by Th8;

      

       A7: p > 2

      proof

        

         A8: (m1 + 1) = m;

        assume

         A9: p <= 2;

        p >= (1 + 1) by A5, NAT_1: 13;

        then 2 divides m1 by A9, XXREAL_0: 1, A4;

        then 2 divides 1 by A8, INT_2: 1, A6;

        hence contradiction by INT_2: 13;

      end;

      then

      reconsider p2 = (p - 2) as Nat by NAT_1: 21;

      reconsider p1 = (p - 1) as Nat by NAT_1: 20, A3, INT_2:def 4;

      set T1 = (p1 -tuples_on F);

      set XFSG1 = { f where f be Element of T1 : Q1[f] & (f . 1) = (f . p1) };

      set XFSG2 = { f where f be Element of T1 : Q1[f] & (f . 1) <> (f . p1) };

      defpred C[ object, object] means for f be FinSequence st f = $1 holds $2 = (f | p1);

      

       A10: for x be object st x in F holds W(x) in ( bool F)

      proof

        let x be object;

        assume x in F;

         W(x) c= F

        proof

          let y be object;

          assume y in W(x);

          then [x, y] in FSG by RELAT_1: 169;

          hence thesis by RELAT_1: 15;

        end;

        hence thesis;

      end;

      consider IM be Function of F, ( bool F) such that

       A11: for x be object st x in F holds (IM . x) = W(x) from FUNCT_2:sch 2( A10);

      

       A12: for x st x in F holds ( card (IM . x)) = m

      proof

        let y;

        assume

         A13: y in F;

        

        hence ( card (IM . y)) = ( card W(y)) by A11

        .= m by A2, Th11, A1, A13;

      end;

      defpred Q[ FinSequence] means [($1 . p), ($1 . 1)] in FSG & Q1[$1];

      set T = (p -tuples_on F);

      set XT = { f where f be Element of T : Q[f] };

      set XFSG = { f where f be Element of ((p2 + 1) -tuples_on F) : (f . 1) in F & for i be Nat st i in ( Seg p2) holds (f . (i + 1)) in (IM . (f . i)) };

      F c= F;

      then

       A14: ( card XFSG) = (( card F) * (m |^ p2)) by A12, Th6;

      then

      reconsider XFSG as finite set;

      

       A15: for f be Element of (p1 -tuples_on F) holds f in XFSG iff Q1[f]

      proof

        let f be Element of T1;

        

         A16: ( len f) = (p2 + 1) by CARD_1:def 7;

        hereby

          assume f in XFSG;

          then

           A17: ex g be Element of T1 st f = g & (g . 1) in F & for i be Nat st i in ( Seg p2) holds (g . (i + 1)) in (IM . (g . i));

          thus Q1[f]

          proof

            let i such that

             A18: 1 <= i and

             A19: i < ( len f);

            i in ( dom f) by A18, A19, FINSEQ_3: 25;

            then (f . i) in ( rng f) by FUNCT_1:def 3;

            then

             A20: W(.) = (IM . (f . i)) by A11;

            i <= p2 by A19, A16, NAT_1: 13;

            then i in ( Seg p2) by A18;

            hence thesis by A17, A20, RELAT_1: 169;

          end;

        end;

        assume

         A21: Q1[f];

        

         A22: for i be Nat st i in ( Seg p2) holds (f . (i + 1)) in (IM . (f . i))

        proof

          let i be Nat;

          assume

           A23: i in ( Seg p2);

          then

           A24: 1 <= i by FINSEQ_1: 1;

          i <= p2 by A23, FINSEQ_1: 1;

          then

           A25: i < (p2 + 1) by NAT_1: 13;

          then i in ( dom f) by A24, A16, FINSEQ_3: 25;

          then

           A26: (f . i) in ( rng f) by FUNCT_1:def 3;

           [(f . i), (f . (i + 1))] in FSG by A24, A25, A21, A16;

          then (f . (i + 1)) in W(.) by RELAT_1: 169;

          hence thesis by A26, A11;

        end;

        1 <= ( len f) by A16, NAT_1: 11;

        then 1 in ( dom f) by FINSEQ_3: 25;

        then (f . 1) in ( rng f) by FUNCT_1:def 3;

        hence thesis by A22;

      end;

      

       A27: XFSG1 c= XFSG

      proof

        let x be object;

        assume x in XFSG1;

        then ex f be Element of T1 st x = f & Q1[f] & (f . 1) = (f . p1);

        hence thesis by A15;

      end;

      

       A28: XFSG2 c= XFSG

      proof

        let x be object;

        assume x in XFSG2;

        then ex f be Element of T1 st x = f & Q1[f] & (f . 1) <> (f . p1);

        hence thesis by A15;

      end;

      then

      reconsider XFSG1, XFSG2 as finite set by A27;

      

       A29: p > 1 by A3, INT_2:def 4;

      then not p divides (m1 + 1) by A4, NEWTON: 39;

      then

       A30: not p divides (m |^ p2) by A3, NAT_3: 5;

      

       A31: XFSG1 misses XFSG2

      proof

        assume XFSG1 meets XFSG2;

        then

        consider x be object such that

         A32: x in XFSG1 & x in XFSG2 by XBOOLE_0: 3;

        (ex f be Element of T1 st x = f & Q1[f] & (f . 1) = (f . p1)) & ex f be Element of T1 st x = f & Q1[f] & (f . 1) <> (f . p1) by A32;

        hence contradiction;

      end;

      

       A33: for x be object st x in XT holds ex y be object st y in XFSG & C[x, y]

      proof

        let x be object;

        assume x in XT;

        then

        consider f be Element of T such that

         A34: x = f and

         A35: Q[f];

        set g = (f | p1);

        

         A36: ( len f) = (p1 + 1) by CARD_1:def 7;

        then p1 < ( len f) by NAT_1: 13;

        then

         A37: ( len g) = p1 by FINSEQ_1: 59;

        then

        reconsider g as Element of T1 by FINSEQ_2: 92;

        take g;

         Q1[g]

        proof

          let i be Nat;

          assume that

           A38: 1 <= i and

           A39: i < ( len g);

          i in ( dom g) by A38, A39, FINSEQ_3: 25;

          then

           A40: (f . i) = (g . i) by FUNCT_1: 47;

          i < ( len f) by A39, A36, NAT_1: 13, A37;

          then

           A41: [(f . i), (f . (i + 1))] in FSG by A38, A35;

          1 < (i + 1) & (i + 1) <= ( len g) by A38, NAT_1: 13, A39;

          then (i + 1) in ( dom g) by FINSEQ_3: 25;

          hence thesis by A40, FUNCT_1: 47, A41;

        end;

        hence thesis by A15, A34;

      end;

      consider FSGR be Function of XT, XFSG such that

       A42: for x be object st x in XT holds C[x, (FSGR . x)] from FUNCT_2:sch 1( A33);

      reconsider pr = (FSGR ~ ) as Relation;

      m > 2 by Th10, A1, A2;

      then (m |^ p2) > 0 by NEWTON: 83;

      then

       A43: XFSG is non empty by XREAL_1: 129, A14;

      then

       A44: ( dom FSGR) = XT by FUNCT_2:def 1;

      

       A45: XFSG c= (XFSG1 \/ XFSG2)

      proof

        let x be object;

        assume

         A46: x in XFSG;

        then

        consider f be Element of ((p2 + 1) -tuples_on F) such that

         A47: x = f and (f . 1) in F & for i be Nat st i in ( Seg p2) holds (f . (i + 1)) in (IM . (f . i));

        

         A48: (f . 1) = (f . p1) or (f . 1) <> (f . p1);

         Q1[f] by A15, A46, A47;

        then f in XFSG1 or f in XFSG2 by A48;

        hence thesis by XBOOLE_0:def 3, A47;

      end;

      

       A49: p = (p1 + 1);

      then

       A50: p1 >= 1 by A29, NAT_1: 13;

      

       A51: for f be Element of T1 st Q1[f] & [(f . p1), y] in FSG & [y, (f . 1)] in FSG holds (f ^ <*y*>) in XT

      proof

        let f be Element of T1 such that

         A52: Q1[f] and

         A53: [(f . p1), y] in FSG and

         A54: [y, (f . 1)] in FSG;

        set fy = (f ^ <*y*>);

        y in F by A53, RELAT_1: 15;

        then <*y*> is FinSequence of F by FINSEQ_1: 74;

        then

         A55: fy is FinSequence of F by FINSEQ_1: 75;

        

         A56: ( len fy) = (p1 + 1) by CARD_1:def 7;

        

         A57: ( len f) = p1 by CARD_1:def 7;

        then

         A58: (fy . p) = y by FINSEQ_1: 42;

        reconsider fy as Element of T by A55, A56, FINSEQ_2: 92;

        

         A59: Q1[fy]

        proof

          let i such that

           A60: 1 <= i and

           A61: i < ( len fy);

          

           A62: i <= p1 by A61, A56, NAT_1: 13;

          then

           A63: i in ( dom f) by A60, A57, FINSEQ_3: 25;

          then

           A64: (f . i) = (fy . i) by FINSEQ_1:def 7;

          per cases by A62, XXREAL_0: 1;

            suppose i = p1;

            hence thesis by A58, A63, FINSEQ_1:def 7, A53;

          end;

            suppose

             A65: i < p1;

            then (i + 1) <= p1 by NAT_1: 13;

            then

             A66: (i + 1) in ( dom f) by NAT_1: 11, A57, FINSEQ_3: 25;

             [(f . i), (f . (i + 1))] in FSG by A65, A57, A52, A60;

            hence thesis by A66, FINSEQ_1:def 7, A64;

          end;

        end;

        1 in ( dom f) by A50, A57, FINSEQ_3: 25;

        then [(fy . p), (fy . 1)] in FSG by FINSEQ_1:def 7, A58, A54;

        hence thesis by A59;

      end;

      

       A67: for f be Element of T1 st Q1[f] & (f . 1) = (f . p1) holds for y st y in ( Im (FSG,(f . 1))) holds (f ^ <*y*>) in XT

      proof

        let f be Element of T1 such that

         A68: Q1[f] & (f . 1) = (f . p1);

        let y such that

         A69: y in ( Im (FSG,(f . 1)));

        

         A70: [(f . 1), y] in FSG by RELAT_1: 169, A69;

        then [y, (f . 1)] in FSG by Lm3;

        hence thesis by A68, A70, A51;

      end;

      

       A71: for x st x in XFSG1 holds ( card ( Im (pr,x))) = m

      proof

        let x;

        assume x in XFSG1;

        then

        consider f be Element of T1 such that

         A72: f = x and

         A73: Q1[f] & (f . 1) = (f . p1);

        deffunc D( object) = (f ^ <*$1*>);

        

         A74: ( len f) = p1 by CARD_1:def 7;

        

         A75: for y be object st y in ( Im (FSG,(f . 1))) holds D(y) in ( Im (pr,f))

        proof

          let y be object;

          assume

           A76: y in ( Im (FSG,(f . 1)));

          then

           A77: D(y) in XT by A67, A73;

          then

          consider fy be Element of T such that

           A78: D(y) = fy and Q[fy];

          reconsider yy = <*y*> as FinSequence of F by A78, FINSEQ_1: 36;

          (FSGR . D(y)) = ((f ^ yy) | p1) by A76, A67, A73, A42

          .= f by A74, FINSEQ_5: 23;

          then [fy, f] in FSGR by A77, A78, A44, FUNCT_1:def 2;

          then [f, fy] in pr by RELAT_1:def 7;

          hence thesis by A78, RELAT_1: 169;

        end;

        consider d be Function of ( Im (FSG,(f . 1))), ( Im (pr,f)) such that

         A79: for y be object st y in ( Im (FSG,(f . 1))) holds (d . y) = D(y) from FUNCT_2:sch 2( A75);

        

         A80: d is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A81: x1 in ( dom d) and

           A82: x2 in ( dom d) & (d . x1) = (d . x2);

          (d . x1) = D(x1) by A81, A79;

          then D(x1) = D(x2) by A82, A79;

          hence thesis by FINSEQ_2: 17;

        end;

        

         A83: 1 in ( dom f) by A74, A50, FINSEQ_3: 25;

        then (f . 1) in ( rng f) by FUNCT_1:def 3;

        then

         A84: ( card ( Im (FSG,(f . 1)))) = m by A1, Th11, A2;

        then ( Im (FSG,(f . 1))) is non empty by Th10, A1, A2;

        then ex xx be object st xx in ( Im (FSG,(f . 1)));

        then ( Im (pr,f)) is non empty by A75;

        then

         A85: ( dom d) = ( Im (FSG,(f . 1))) by FUNCT_2:def 1;

        ( Im (pr,f)) c= ( rng d)

        proof

          let y be object;

          assume y in ( Im (pr,f));

          then [f, y] in pr by RELAT_1: 169;

          then

           A86: [y, f] in FSGR by RELAT_1:def 7;

          then

           A87: y in ( dom FSGR) by XTUPLE_0:def 12;

          then

          consider g be Element of T such that

           A88: y = g and

           A89: Q[g] by A44;

          

           A90: ( len g) = (p1 + 1) by CARD_1:def 7;

          f = (FSGR . y) by A87, A86, FUNCT_1:def 2;

          then (g | p1) = f by A87, A42, A88;

          then

           A91: g = (f ^ <*(g . p)*>) by A90, FINSEQ_3: 55;

          then (g . 1) = (f . 1) by A83, FINSEQ_1:def 7;

          then

           A92: [(f . 1), (g . p)] in FSG by A89, Lm3;

          then (g . p) in ( dom d) by RELAT_1: 169, A85;

          then (d . (g . p)) in ( rng d) by FUNCT_1:def 3;

          hence thesis by A92, RELAT_1: 169, A91, A79, A88;

        end;

        then ( Im (pr,f)) = ( rng d);

        hence thesis by A85, A80, WELLORD2:def 4, A84, CARD_1: 5, A72;

      end;

      (XFSG1 \/ XFSG2) c= XFSG by A27, XBOOLE_1: 8, A28;

      then

       A93: XFSG = (XFSG1 \/ XFSG2) by A45;

      then ( card XFSG) = (( card XFSG1) + ( card XFSG2)) by A31, CARD_2: 40;

      then

       A94: ((1 + (m * m1)) * (m |^ p2)) = (( card XFSG1) + ( card XFSG2)) by A14, A1, A2, Th12;

      

       A95: for f be Element of T1 st Q1[f] & (f . 1) <> (f . p1) holds ex y st y in F & (f ^ <*y*>) in XT

      proof

        let f be Element of T1 such that

         A96: Q1[f] and

         A97: (f . 1) <> (f . p1);

        

         A98: ( len f) = p1 by CARD_1:def 7;

        then p1 in ( dom f) by A50, FINSEQ_3: 25;

        then

         A99: (f . p1) in ( rng f) by FUNCT_1:def 3;

        1 in ( dom f) by A98, A50, FINSEQ_3: 25;

        then (f . 1) in ( rng f) by FUNCT_1:def 3;

        then

        consider w be object such that

         A100: {w} = (( Im (FSG,(f . p1))) /\ ( Coim (FSG,(f . 1)))) by A99, A97, Def3;

        take w;

        

         A101: w in {w} by TARSKI:def 1;

        ( Coim (FSG,(f . 1))) = ( Im (FSG,(f . 1))) by Th2;

        then w in ( Im (FSG,(f . 1))) by A101, A100, XBOOLE_0:def 4;

        then [(f . 1), w] in FSG by RELAT_1: 169;

        then

         A102: [w, (f . 1)] in FSG by Lm3;

        w in ( Im (FSG,(f . p1))) by A101, A100, XBOOLE_0:def 4;

        then [(f . p1), w] in FSG by RELAT_1: 169;

        hence thesis by A102, A51, A96, RELAT_1: 15;

      end;

      

       A103: for x st x in XFSG2 holds ( card ( Im ((pr | XFSG2),x))) = 1

      proof

        let x such that

         A104: x in XFSG2;

        consider f be Element of T1 such that

         A105: x = f and

         A106: Q1[f] and

         A107: (f . 1) <> (f . p1) by A104;

        consider y such that y in F and

         A109: (f ^ <*y*>) in XT by A95, A106, A107;

        

         A111: ( len f) = p1 by CARD_1:def 7;

        

         A112: ( Im ((pr | XFSG2),f)) c= {(f ^ <*y*>)}

        proof

          let z be object;

          consider w be Element of T such that

           A113: w = (f ^ <*y*>) and

           A114: Q[w] by A109;

          

           A115: (w . p) = y by A113, A111, FINSEQ_1: 42;

          

           A116: p1 in ( dom f) by A50, A111, FINSEQ_3: 25;

          then

           A117: (w . p1) = (f . p1) by A113, FINSEQ_1:def 7;

          

           A118: 1 in ( dom f) by A50, A111, FINSEQ_3: 25;

          then

           A119: (w . 1) = (f . 1) by A113, FINSEQ_1:def 7;

          assume z in ( Im ((pr | XFSG2),f));

          then [f, z] in (pr | XFSG2) by RELAT_1: 169;

          then [f, z] in pr by RELAT_1:def 11;

          then

           A120: [z, f] in FSGR by RELAT_1:def 7;

          then

           A121: z in ( dom FSGR) by XTUPLE_0:def 12;

          then z in XT;

          then

          consider g be Element of T such that

           A122: g = z and

           A123: Q[g];

          

           A124: p1 < p by A49, NAT_1: 13;

          f = (FSGR . z) by A121, FUNCT_1:def 2, A120;

          then

           A125: f = (g | p1) by A121, A42, A122;

          then

           A126: (g . 1) = (f . 1) by A118, FUNCT_1: 47;

          ( len w) = p by CARD_1:def 7;

          then

           A127: [(w . p1), (w . p)] in FSG by A49, A29, NAT_1: 13, A124, A114;

          

           A128: ( len g) = p by CARD_1:def 7;

          then

           A129: g = (f ^ <*(g . p)*>) by A125, FINSEQ_3: 55;

          

           A130: (g . p1) = (f . p1) by A116, A125, FUNCT_1: 47;

           [(g . p1), (g . p)] in FSG by A49, A29, NAT_1: 13, A124, A123, A128;

          then (g . p) = (w . p) by A119, A126, A117, A130, A123, A114, A107, A127, Lm5;

          hence thesis by A129, A115, A122, TARSKI:def 1;

        end;

        (FSGR . (f ^ <*y*>)) = ((f ^ <*y*>) | p1) by A42, A109

        .= f by FINSEQ_5: 23, A111;

        then [(f ^ <*y*>), f] in FSGR by FUNCT_1:def 2, A44, A109;

        then [f, (f ^ <*y*>)] in pr by RELAT_1:def 7;

        then [f, (f ^ <*y*>)] in (pr | XFSG2) by A105, A104, RELAT_1:def 11;

        then (f ^ <*y*>) in ( Im ((pr | XFSG2),f)) by RELAT_1: 169;

        then ( Im ((pr | XFSG2),f)) = {(f ^ <*y*>)} by A112, ZFMISC_1: 33;

        hence thesis by A105, CARD_1: 30;

      end;

      (( dom (pr | XFSG2)) \ XFSG2) = {} by RELAT_1: 58, XBOOLE_1: 37;

      then ( card ((pr | XFSG2) | (( dom (pr | XFSG2)) \ XFSG2))) = 0 ;

      

      then

       A131: ( card (pr | XFSG2)) = ( 0 +` (1 *` ( card XFSG2))) by A103, SIMPLEX1: 1

      .= (1 *` ( card XFSG2)) by CARD_2: 18

      .= ( card XFSG2) by CARD_2: 21;

      XFSG c= ( rng FSGR)

      proof

        let xp be object;

        assume

         A132: xp in XFSG;

        per cases by A132, A45, XBOOLE_0:def 3;

          suppose xp in XFSG1;

          then

          consider f be Element of T1 such that

           A133: xp = f and

           A134: Q1[f] & (f . 1) = (f . p1);

          ( len f) = p1 by CARD_1:def 7;

          then 1 in ( dom f) by A50, FINSEQ_3: 25;

          then (f . 1) in ( rng f) by FUNCT_1:def 3;

          then ( card ( Im (FSG,(f . 1)))) = m by A1, Th11, A2;

          then ( Im (FSG,(f . 1))) is non empty by Th10, A1, A2;

          then

          consider y be object such that

           A135: y in ( Im (FSG,(f . 1)));

          set fy = y;

          set fy = (f ^ <*y*>);

          (f ^ <*y*>) in XT by A67, A134, A135;

          then

           A136: (FSGR . fy) in ( rng FSGR) by A44, FUNCT_1:def 3;

           [(f . 1), y] in FSG by A135, RELAT_1: 169;

          then y in F by RELAT_1: 15;

          then <*y*> is FinSequence of F by FINSEQ_1: 74;

          then

           A138: ( len fy) = (p1 + 1) & fy is FinSequence of F by CARD_1:def 7, FINSEQ_1: 75;

          

           A139: ( len f) = p1 by CARD_1:def 7;

          (FSGR . fy) = (fy | p1) by A42, A67, A134, A135;

          hence thesis by A139, FINSEQ_5: 23, A133, A136;

          reconsider fy as Element of T by A138, FINSEQ_2: 92;

        end;

          suppose xp in XFSG2;

          then

          consider f be Element of T1 such that

           A140: xp = f and

           A141: Q1[f] & (f . 1) <> (f . p1);

          consider y such that

           A142: y in F and

           A143: (f ^ <*y*>) in XT by A141, A95;

          set fy = (f ^ <*y*>);

          

           A144: (FSGR . fy) = (fy | p1) & (FSGR . fy) in ( rng FSGR) by A42, A143, A44, FUNCT_1:def 3;

           <*y*> is FinSequence of F by A142, FINSEQ_1: 74;

          then ( len fy) = (p1 + 1) & fy is FinSequence of F by CARD_1:def 7, FINSEQ_1: 75;

          then

          reconsider fy as Element of T by FINSEQ_2: 92;

          ( len f) = p1 by CARD_1:def 7;

          hence thesis by FINSEQ_5: 23, A140, A144;

        end;

      end;

      then XFSG = ( rng FSGR);

      then ( dom pr) = XFSG by RELAT_1: 20;

      then (( dom pr) \ XFSG1) = XFSG2 by XBOOLE_1: 88, A93, A31;

      

      then

       A146: ( card pr) = (( card XFSG2) +` (m *` ( card XFSG1))) by A131, A71, SIMPLEX1: 1

      .= (( card XFSG2) +` (m * ( card XFSG1))) by Lm1

      .= (( card XFSG2) + (m * ( card XFSG1))) by Lm1;

      

       A147: for f1,f2 be FinSequence of F st (f1 ^ f2) is p -element & Q[(f1 ^ f2)] holds Q[(f2 ^ f1)]

      proof

        let f1,f2 be FinSequence of F;

        assume that

         A148: (f1 ^ f2) is p -element and

         A149: Q[(f1 ^ f2)];

        set f12 = (f1 ^ f2), f21 = (f2 ^ f1), L1 = ( len f1), L2 = ( len f2);

        

         A150: ( len f12) = p by CARD_1:def 7, A148;

        

         A151: ( len f21) = (L2 + L1) by FINSEQ_1: 22;

        

         A152: ( len f12) = (L1 + L2) by FINSEQ_1: 22;

        per cases ;

          suppose f1 = {} or f2 = {} ;

          then f12 = f2 & f21 = f2 or f12 = f1 & f21 = f1 by FINSEQ_1: 34;

          hence thesis by A149;

        end;

          suppose

           A153: f1 <> {} & f2 <> {} ;

          then L2 >= 1 by FINSEQ_1: 20;

          then

           A154: 1 in ( dom f2) by FINSEQ_3: 25;

          then

           A155: (f12 . (L1 + 1)) = (f2 . 1) by FINSEQ_1:def 7;

          

           A156: (L1 + 1) <= p by A153, FINSEQ_1: 20, A150, A152, XREAL_1: 6;

          

           A157: L1 >= 1 by A153, FINSEQ_1: 20;

          then

           A158: 1 in ( dom f1) by FINSEQ_3: 25;

          

           A159: L1 in ( dom f1) by A157, FINSEQ_3: 25;

          then

           A160: (f21 . p) = (f1 . L1) by A150, A152, FINSEQ_1:def 7;

          (f12 . L1) = (f1 . L1) by A159, FINSEQ_1:def 7;

          then [(f1 . L1), (f2 . 1)] in FSG by A156, NAT_1: 13, A149, A157, A155, A150;

          hence [(f21 . p), (f21 . 1)] in FSG by A160, A154, FINSEQ_1:def 7;

          let i;

          assume that

           A161: 1 <= i and

           A162: i < ( len f21);

          

           A163: i in ( dom f21) by A161, A162, FINSEQ_3: 25;

          per cases by A163, FINSEQ_1: 25;

            suppose

             A164: i in ( dom f2);

            then

             A165: i <= L2 by FINSEQ_3: 25;

            

             A166: (f21 . i) = (f2 . i) by A164, FINSEQ_1:def 7;

            per cases ;

              suppose

               A167: i = L2;

              

               A168: (f1 . 1) = (f12 . 1) by A158, FINSEQ_1:def 7;

              (f2 . i) = (f12 . p) by A167, A150, A152, A164, FINSEQ_1:def 7;

              hence thesis by A168, A167, A158, FINSEQ_1:def 7, A149, A166;

            end;

              suppose

               A169: i <> L2;

              

               A170: (1 + 0 ) <= (L1 + i) by XREAL_1: 7, A157;

              

               A171: i < L2 by A169, A165, XXREAL_0: 1;

              then (L1 + i) < p by A150, A152, XREAL_1: 6;

              then

               A172: [(f12 . (L1 + i)), (f12 . ((L1 + i) + 1))] in FSG by A170, A149, A150;

              

               A173: (f12 . (L1 + i)) = (f2 . i) by A164, FINSEQ_1:def 7;

              (i + 1) <= L2 by A171, NAT_1: 13;

              then

               A174: (i + 1) in ( dom f2) by NAT_1: 11, FINSEQ_3: 25;

              then (f12 . (L1 + (i + 1))) = (f2 . (i + 1)) by FINSEQ_1:def 7;

              hence thesis by A174, FINSEQ_1:def 7, A172, A173, A166;

            end;

          end;

            suppose ex n be Nat st n in ( dom f1) & i = (L2 + n);

            then

            consider n be Nat such that

             A175: n in ( dom f1) and

             A176: i = (L2 + n);

            

             A177: (f21 . i) = (f1 . n) & (f12 . n) = (f1 . n) by A175, A176, FINSEQ_1:def 7;

            

             A178: 1 <= n by A175, FINSEQ_3: 25;

            

             A179: n < L1 by A176, A162, A151, XREAL_1: 6;

            then

             A180: (n + 0 ) < (L1 + L2) by XREAL_1: 8;

            (n + 1) <= L1 by A179, NAT_1: 13;

            then

             A181: (n + 1) in ( dom f1) by NAT_1: 11, FINSEQ_3: 25;

            (i + 1) = (L2 + (n + 1)) by A176;

            then

             A182: (f21 . (i + 1)) = (f1 . (n + 1)) by A181, FINSEQ_1:def 7;

            (f12 . (n + 1)) = (f1 . (n + 1)) by A181, FINSEQ_1:def 7;

            hence thesis by A178, A180, A149, A152, A177, A182;

          end;

        end;

      end;

      

       A183: for f1 be Element of T st Q[f1] holds for i be Nat st i < p & f1 = ((f1 /^ i) ^ (f1 | i)) holds i = 0

      proof

        let f1 be Element of T such that

         A184: Q[f1];

        

         A185: ( len f1) = p by CARD_1:def 7;

        then 2 in ( dom f1) by A7, FINSEQ_3: 25;

        then

         A186: (f1 . 2) in ( rng f1) by FUNCT_1:def 3;

        let i be Nat such that

         A187: i < p & f1 = ((f1 /^ i) ^ (f1 | i)) & i <> 0 ;

        ( rng f1) c= {(f1 . 1)} by A187, A185, A3, Th7;

        then

         A188: (f1 . 2) = (f1 . 1) by A186, TARSKI:def 1;

         [(f1 . 1), (f1 . (1 + 1))] in FSG by A3, INT_2:def 4, A184, A185;

        hence contradiction by A188, Lm2;

      end;

      consider C be Cardinal such that

       A189: (p *` C) = ( card XT) from Sch( A147, A183);

      

       A190: ( card pr) = ( card FSGR) by Th1

      .= ( card ( dom FSGR)) by CARD_1: 62

      .= ( card XT) by A43, FUNCT_2:def 1;

      then C is finite by A146, A189;

      then

      reconsider C as Nat;

      (p * C) = (( card XFSG2) + (m * ( card XFSG1))) by A189, Lm1, A146, A190;

      then

       A191: p divides (((1 + (m * m1)) * (m |^ p2)) + ((m - 1) * ( card XFSG1))) by A94, INT_1:def 3;

       not p divides ((m * m1) + 1) by A4, INT_2: 2, NEWTON: 39, A29;

      then

       A192: not p divides ((1 + (m * m1)) * (m |^ p2)) by A30, A3, INT_5: 7;

      p divides (m1 * ( card XFSG1)) by A4, INT_2: 2;

      hence contradiction by A192, INT_2: 1, A191;

    end;