let V be non empty addLoopStr ; :: thesis: for A being Subset of V

for v being Element of V holds card (v + A) c= card A

let A be Subset of V; :: thesis: for v being Element of V holds card (v + A) c= card A

let v be Element of V; :: thesis: card (v + A) c= card A

deffunc H_{1}( Element of V) -> Element of the carrier of V = v + $1;

card { H_{1}(w) where w is Element of V : w in A } c= card A
from TREES_2:sch 2();

hence card (v + A) c= card A ; :: thesis: verum

for v being Element of V holds card (v + A) c= card A

let A be Subset of V; :: thesis: for v being Element of V holds card (v + A) c= card A

let v be Element of V; :: thesis: card (v + A) c= card A

deffunc H

card { H

hence card (v + A) c= card A ; :: thesis: verum