set a = the non empty homogeneous quasi_total PartFunc of (A *),A;
reconsider a = the non empty homogeneous quasi_total PartFunc of (A *),A as Element of PFuncs ((A *),A) by PARTFUN1:45;
take <*a*> ; :: thesis: ( <*a*> is homogeneous & <*a*> is quasi_total & <*a*> is non-empty & not <*a*> is empty )
hereby :: according to MARGREL1:def 23 :: thesis: ( <*a*> is quasi_total & <*a*> is non-empty & not <*a*> is empty )
let n be Nat; :: thesis: for h being PartFunc of (A *),A st n in dom <*a*> & h = <*a*> . n holds
h is homogeneous
let h be PartFunc of (A *),A; :: thesis: ( n in dom <*a*> & h = <*a*> . n implies h is homogeneous )
assume n in dom <*a*> ; :: thesis: ( h = <*a*> . n implies h is homogeneous )
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2, TARSKI:def 1;
hence ( h = <*a*> . n implies h is homogeneous ) by FINSEQ_1:40; :: thesis: verum
end;
hereby :: according to MARGREL1:def 24 :: thesis: ( <*a*> is non-empty & not <*a*> is empty )
let n be Nat; :: thesis: for h being PartFunc of (A *),A st n in dom <*a*> & h = <*a*> . n holds
h is quasi_total
let h be PartFunc of (A *),A; :: thesis: ( n in dom <*a*> & h = <*a*> . n implies h is quasi_total )
assume n in dom <*a*> ; :: thesis: ( h = <*a*> . n implies h is quasi_total )
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2, TARSKI:def 1;
hence ( h = <*a*> . n implies h is quasi_total ) by FINSEQ_1:40; :: thesis: verum
end;
hereby :: according to FUNCT_1:def 9 :: thesis: not <*a*> is empty
let n be object ; :: thesis: ( n in dom <*a*> implies not <*a*> . n is empty )
assume n in dom <*a*> ; :: thesis: not <*a*> . n is empty
then n in Seg 1 by FINSEQ_1:38;
then n = 1 by FINSEQ_1:2, TARSKI:def 1;
hence not <*a*> . n is empty by FINSEQ_1:40; :: thesis: verum
end;
thus not <*a*> is empty ; :: thesis: verum