let S be non empty finite set ; :: thesis: for x being Element of S holds
( x in rng (canFS S) & ex n being Nat st
( n in dom (canFS S) & x = (canFS S) . n & n in Seg (card S) ) )
let x be Element of S; :: thesis: ( x in rng (canFS S) & ex n being Nat st
( n in dom (canFS S) & x = (canFS S) . n & n in Seg (card S) ) )
A1: x in S ;
then x in rng (canFS S) by FUNCT_2:def 3;
then consider n being object such that
A2: ( n in dom (canFS S) & x = (canFS S) . n ) by FUNCT_1:def 3;
reconsider n = n as Nat by A2;
len (canFS S) = card S by FINSEQ_1:93;
then n in Seg (card S) by A2, FINSEQ_1:def 3;
hence ( x in rng (canFS S) & ex n being Nat st
( n in dom (canFS S) & x = (canFS S) . n & n in Seg (card S) ) ) by A2, A1, FUNCT_2:def 3; :: thesis: verum